Have a look at Church’s (first) Set Theory with a Universal Set, which is equiconsistent with ZFGC, though Church didn’t publish a full proof, and I think he abandoned the proof in his archives at Princeton. (My forthcoming doctoral thesis completes the proof for a variant with the singleton function as a set.) His archives also contain lecture notes on some more complicated theories with approximately the same name, but I believe he gave up on those theories, not just the details of the consistency proofs. • Alonzo Church (1974). “Set Theory with a Universal Set,” [Proceedings of the Tarski Symposium][1]. Proceedings of Symposia in Pure Mathematics XXV, ed. L. Henkin, American Mathematical Society, pp. 297–308. • T. E. Forster (1995). Set Theory with a Universal Set: Exploring an Untyped Universe (Oxford Logic Guides 31). Oxford University Press. ISBN 0-19-851477-8. • T. E. Forster (2001). “[Church’s Set Theory with a Universal Set.][2]” See also the [Wikipedia article][3] (disclaimer: I started it in its current form.) [1]: http://www.ams.org/books/pspum/025/pspum025-endmatter.pdf [2]: http://www.dpmms.cam.ac.uk/~tf/church2001.ps [3]: https://en.wikipedia.org/wiki/Universal_set