Consider *General Set Theory* ($ \mathsf { GST } $) axiomatized by the following.

**Axiom of Extensionality:**The sets $ x $ and $ y $ are the same set if they have the same members: $$ \forall x \forall y \bigl ( \forall z ( z \in x \leftrightarrow z \in y ) \rightarrow x = y \bigr ) \text . $$**Axiom of Adjunction:**If $ x $ and $ y $ are sets, then there exists a set whose members are just $ y $ and the members of $ x $: $$ \forall x \forall y \exists z \forall w ( w \in z \leftrightarrow w \in x \lor w = y ) $$**Axiom Schema of Separation:**If $ x $ is a set and $ \phi $ is any property, then there exists a set $ y $ containing just those elements $ z $ in $ x $ which satisfy the property $ \phi $: $$ \forall x \exists y \forall z \bigl ( z \in y \leftrightarrow z \in x \land \phi ( z ) \bigr ) \text . $$

It's rather straightforward to verify that $ \mathsf { GST } $ proves the existence of every hereditarily finite set; i.e. $ \mathsf { GST } \vdash \exists ! x \, \phi ( x ) $ for some formula $ \phi $ defining the intended set. Since the family of hereditarily finite sets gives a model $ \mathfrak M $ of $ \mathsf { GST } $, those are the only sets that provably exist. My question is the validity of the following statement:

If $ \mathsf { GST } \vdash \exists ! x \, \phi ( x ) $, $ \mathsf { GST } \vdash \exists ! x \, \psi ( x ) $ and $ \mathfrak M \models \forall x \forall y \bigl ( \phi ( x ) \land \psi ( y ) \rightarrow x = y \bigr ) $, then $ \mathsf { GST } \vdash \forall x \forall y \bigl ( \phi ( x ) \land \psi ( y ) \rightarrow x = y \bigr ) $.

My motivation is the fact that $ \mathsf { GST } $ is mutually interpretable with $ \mathsf { PA } $. For $ \mathsf { PA } $ (and even much weaker arithmetical theories like Robinson's) we know the following:

- For every $ n \in \mathbb N $ there is a numeral $ \overline n $ in the language, which is interpreted as $ n $ in the standard model.
- As $ \mathbb N $ gives a model of $ \mathsf { PA } $, natural numbers are the only objects that $ \mathsf { PA } $ proves to exist.
- The equality relation between natural numbers is representable in $ \mathsf { PA } $ in the sense that for any $ m , n \in \mathbb N $, $ m = n $ implies $ \mathsf { PA } \vdash \overline m = \overline n $, and $ m \ne n $ impiles $ \mathsf { PA } \vdash \neg \, \overline m = \overline n $.

My question stated above is about representability of equality of hereditarily finite sets in $ \mathsf { GST } $. The similarities explained above make me feel that it must be true.

I understand that $ \mathsf { GST } $ might not be strong enough for proving the desired representability, and one might need to strengthen it (as the family of hereditarily finite sets gives a model for $ \mathsf { ZFC } $ without infinity, we can see that much stronger candidates are available). But since very weak arithmetical theories are enough for proving representability of equality for natural numbers, I suspect that no additional strength would be necessary for set theoris either.

**P.S.** I've only seen the claim that $ \mathsf { GST } $ and $ \mathsf { PA } $ are mutually interpretable in a couple of sources. I don't know of any sources where a proof can be found. I'd really appreciate it if someone could give a reference in the comments section.