To be explicit, by Zermelo set theory with Choice, ZC, I mean the theory with the same language and axioms as ZFC except not Foundation (also called Regularity) and with the axiom scheme of Separation instead of Replacement. By Global Choice I mean adding a new function symbol $F$ and an axiom:$\forall v[v\neq\emptyset \rightarrow F(v)\in v]$, and extending the Separation scheme to include formulas using $F$.


It is known that the axiom of Global Choice gives a conservative extension of Zermelo Frankel set theory with Choice (ZFC). The proof I know is by Haim Gaifman in his "Local and Global Choice Functions" (Israel J. of Math v. 22 nos. 3-4, 1975, pp. 257--265. And there is one I have not worked through which uses forcing by Ulrich Felgner "[Comparison of the axioms of local and universal choice](https://eudml.org/doc/214318)" Fund. Math. 71, 1971, pp. 43-62. Both seem to require the idea of the rank of a set. Maybe one can be adapted to work for ZC, but I do not see it.


Or is there some other proof? Or a disproof?



Is Global Choice conservative over Zermelo with Choice?
The known proofs of conservativity of ZF + GC (Global Choice) over ZFC make significant use of replacement, and as far as I know the problem of conservativity of Z + GC over ZC is wide open. 


Let me add that I have discussed the problem with a number of experts over the past two decades, and also posed it on FOM in 2006 in [this posting](https://cs.nyu.edu/pipermail/fom/2006-February/010080.html).


