This question is about synonymy of $\sf ZFC$ set theory with the following Mereological theory:

Language: first order logic with equality. Extra-logical primitives: $\subseteq$ standing for the binary relation "is a part of", and a total unary function symbol $\{\}$ standing for "is the label of", or can also be read as "is the singleton of".

Extra-logical Axioms:

Parthood: $x \subseteq x \\ x \subseteq y \subseteq x \to x=y \\ x \subseteq y \subseteq z \to x \subseteq z$

Define: $x \ O \ y \iff \exists z: z \subseteq x \land z \subseteq y$

Supplmentation: $y\not \subseteq x \to \exists z \subseteq y: \neg z \ O \ x$

Define: $\operatorname{atom}(x) \iff \forall y \subseteq x \, (y=x)$

Atomicity: $\forall x \, \exists \text{ atom } y: y \subseteq x $

Define: $ x= \lceil a \mid \varphi \rceil \iff \forall \ \operatorname {atom} \ a \, (a \subseteq x \leftrightarrow \exists y: \varphi(y) \land a \subseteq y) $

Define: $x=\lceil a_1,..,a_n \rceil \iff \forall \operatorname{atom} y \, (y \subseteq x \leftrightarrow y=a_1 \lor .. \lor y=a_n ); \\\text{ if } a_1,..,a_n \text { are atoms}$

Labeling: $\{x\}=\{y\} \to x=y$

Purity: $ \exists x \, (y=\{x\}) \leftrightarrow \operatorname{atom}(y)$

Start: $\exists a \exists b \exists c: a=\{a\} \land b\neq a \land c= \lceil a,b \rceil \land b=\{c\}$

Foundation: $ \exists a \exists b \forall h: \forall x \, ( \{x\} \subseteq h \to x \ O \ h ) \to a \subseteq h \lor b \subseteq h$

Define: $x=\mathcal A \iff x=\{x\} \\ x=\mathcal B \iff x \neq \{x\} \land x=\{\lceil \mathcal A, x\rceil \}$

So, we have: $\mathcal A=\{\mathcal A\}\\ \mathcal B= \{\lceil \mathcal A, \mathcal B \rceil\}$

Replacement: $\varphi(a,b) \land \varphi (a,c) \to b=c \\ \to, \\ \exists A: A= \lceil { a \mid \exists b: \varphi(a,b)}\rceil \leftrightarrow \\ \exists B: B= \lceil b \mid \exists a: \varphi(a,b) \rceil $

Infinity: $\exists x: x \neq \mathcal A \land \forall y: \{y\} \subseteq x \to \{\{y\}\} \subseteq x$

Choice: $\forall x \exists C \forall y \in x: \{C(y)\} \subseteq y$

This theory does not violate any of the tenets of Mereology, though it doesn't adopt the Unrestricted Composition principle.

Define set membership $\in$ as:

$$x \in y \iff \{x\} \subseteq y $$

Call the collection of all sentences written in $\sf FOL(=,\in)$ over the whole domain of this theory (i.e. all quantifiers unrestricted) that are provable in this theory as "$\sf MZFC$", standing for "Mereological $\sf ZFC$".

It should be made clear that $\sf MZFC$ proves the non-existence of an empty set, breaches Foundation a little bit, and that it is fully extensional.

Is this system synonymous with $\sf MZFC$ and with $\sf ZFC$?

Is this system minus Choice synonymous with $\sf ZF$?

This question is related to the question "Is ZFGC, minimally modified to allow two Quine atoms instead of the empty set, synonymous\bi-interpretable with ZFGC?", but the global choice function there played a significant role in the synonymy. Here, we don't have global choice. Also, the Mereological theory presented is a modification of the theory presented in an earlier posting to suit withdrawal of proper classes, and also to suit making the starting atoms definable. The idea is that the definability of the starting atoms $\mathcal A, \mathcal B$ may enable us to achieve synonymy even in absence of global choice, and possibly even absence of axiom of choice.