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?