If we add a primitive binary relation $\sim$ to denote "bisimilarity" relation. Remove the axiom of Extensionality from axioms of $\sf ZFC$, and add:
Bisimilarity: $\forall x \, (x \sim x) \\ \begin{align} \forall x \forall y \, (x \sim y \iff &\forall u \in x \exists w \in y \, (w \sim u) \land \\&\forall w \in y \, \exists u \in x \, (u \sim w)) \end{align} $
Define: $\operatorname {Set}(x) \iff \forall a,b \in x: a \neq b \to a \not \sim b $
We alter the axiom of Power sets to:
Power': $\forall x \exists y: \operatorname {Set}(y) \land \forall z \subseteq x \exists {\sf z} \in y\, ( {\sf z }\sim z)$
Infinity': $\exists x: \operatorname {Set} (x) \land 0 \in x \land \\\forall y \in x \exists z \in x: \forall m (m \in z \leftrightarrow m=y)$
Also replace Replacement by Collection, and keep other axioms of $\sf ZFC$.
Add the following axioms:
Reduction: $\forall a \exists \alpha: \operatorname {Set}(\alpha): a \sim \alpha$
De-Extensionality: $\forall x \not \exists y: \forall {\sf x} (x \equiv {\sf x} \to {\sf x} \in y)$
Where $\equiv$ is coextensionality relation, i.e. having the same members.
Is $\sf ZFC$ interpretable in this system?
