Hopefully it should give a nice topos-theoretic account of ZF, independent of anything about elements etc. The main application of reflection principles that I know of, outside of set-theory, is category theory. All toposes E have finite colimits. 4 given with an elementary one using diagram chasing. Let E be a large topos.
E has finite colimits.
Construct a model of ZF from a topos E with reflection. Should be possible. Anyway, this is far too long. Once again, comments welcome, even if it's to tell me where I'm talking nonsense.