>**Joel Hamkins has detected a gap in the proposed proof below. At the moment I do not know of another strategy to the answer the question, but I am leaving it below as signpost to others who might fall in the same trap that I did :)** >**WARNING: The proposed proof below does not work since swapping two urelements does not preserve the global choice function (even though it preserves the set-theoretical structure)**. This answer uses the same idea as the one given in a comment of mine on James Hanson's answer to [this MO question][1]. The basic idea is that one quick way to rule out the bi-interpretability between two theories is to show that some group arises as an automorphism group of a model of one of the theories, but not the other since it is well-known that bi-interpretable models have the same automorphism group. With the above in mind, it suffices to note that by removing Extensionality from $\mathsf{ZF^*+ GC}$ (equivalently $\mathsf{ZF+GC}$) we can easily build a model of the resulting theory that has an automorphism of order 2 by swapping two urelements. But it is well-known that no model of ZFC can have an automorphism of finite order (basically because in the presence of the axiom of choice, let alone global choice, any set can be "coded" by a subset of ordinals) [1]: https://mathoverflow.net/questions/456649/lists-as-a-foundation-of-mathematics/456652#comment1182864_456652