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" 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?