Sets with same members are member of same sets? Seeking deeper insights on link between extensionality and set equality, with or without FOL equality. I have a question on the close links between extensionality and set equality in ZFC, with or without first order logic (FOL) equality as a primitive inherited by ZFC.
The former seems clear and is covered in Wikipedia and in several MSE posts (here, here, here, and here). We start with FOL equality  and it’s substitution property and state that if two sets are equal the predicate formula for membership is true for one set if and only if it’s true for the other. For a predicate formula with two free variables $\phi(x,y)$, the substitution property of FOL equality can be stated as:
$$A=B\implies \forall x (\phi(x,A)\iff \phi(x,B))$$
If the predicate formula is the membership relationship $\phi(x,y)=x\in y$ we get the definition of set equality inherited from FOL equality.
$$A=B\implies \forall x (x\in A\iff x\in B)$$
This defines set equality but doesn’t establish extensionality because two sets with the same members could theoretically differ in other properties which make them unequal. Extensionality is established by stating the converse of the equality definition as the Axiom of Extensionality.
$$\forall x (x\in A\iff x\in B) \implies A=B$$
One can then combine these into the biconditional which nicely captures both extensionality and the inheritance of FOL equality into set equality, i.e.,the binding of $=$ and $\in$, in one tidy package.
$$A=B\iff \forall x (x\in A\iff x\in B)$$
So far so great.
Things get a bit more vague for me if one assumes FOL without equality (or chooses not to define set equality in terms of it). I understand most set theorists accept FOL with equality but I find it an interesting exercise to establish extensionality and define set equality without using FOL equality to define the latter. Again, Wikipedia and other MSE posts touch on this but don’t lock it down for me.
The first option appears to be to just accept the above biconditional as both the definition of set equality a statement in extensionality. Is this actually an axiom or just a definition of set equality in terms of the primitive membership relation? I am aware of the debates on whether definitions are just axioms so what I am really asking is whether extensionality is simply a byproduct of the definition of set equality or whether the Axiom of Extensionality is embedded in the biconditional as it was when we assumed FOL equality.
What intrigues me even more is the approach of stating the Axiom of extensionality without yet defining set equality.
$$\forall A \forall B (\forall X(X\in A \iff X\in B)\iff \forall Y(A\in Y \iff B \in Y))$$
Wikipedia states this without comment as do a few MSE posts linked above. One comment in one of the posts states that either way (i.e., whether you have FOL equality or not) one will eventually have to prove the above.
This idea that two sets have the same members if and only if they are members of the same sets seems pretty fundamental and interesting in its own right, but I have not been able to find any additional color online or in the standard set theory textbooks (Halmos, Hrbeck & Jech, Hatcher, Kunen, etc.). Wikipedia refers to it as merely the “substitution property” of equality but I don’t see that and it seems like it should have deeper meaning. An answer to this post proves it assuming FOL equality, which I get. I would appreciate one of the set theory gurus here explaining how to define set equality from above without using FOL equality, and if there is any deeper meaning to all this. Much appreciated.
 A: We can find all the discussion regarding equality and extensionality in set theory into: Abraham Fraenkel & Yehoshua Bar-Hillel, Foundations of Set Theory, pages 29-33 of 1958 edition.
We may consider equality as primitive, assuming the relevant axioms: this is the case when set theory is based on predicate logic with equality.
Otherwise, we may introduce equality through a suitable definition based on the only primitive of the system (i.e. $\in$), in which case we have to check that the proposed definition ensure: reflexivity, symmetry, transitivity and substitution.
Regarding the second case, that we are interested in here, there are in turn two possibilities:

This may be done in two ways. Either one consider - following Leibniz - two objects to be equal if every object that contains the one as a member contains also the other [Leibniz defined equality in terms of properties and not classes], or one regards them as equal if they contain the same members.

Thus, we have two choices:
$\text {Eq I}) \: \ x=y \text { iff } \ \forall z (x \in z \leftrightarrow y \in z)$, or
$\text {Eq II}) \: \ x=y \text { iff } \ \forall z (z \in x \leftrightarrow z \in y)$, that can be abbreviated, using the usual definition of $\subseteq$ with: $(x \subseteq y) \land (y \subseteq x)$.
Both definitions provide reflexivity, symmetry, transitivity and "right-substitution", i.e. substitution wrt the right argument of $\in$.
The tautology $x \in z \leftrightarrow x \in z$ gives us reflexivity, and the corresponding properties of $\leftrightarrow$ give symmetry and transitivity.
Regarding "right-substitutivity", i.e. $(z \in x \land x=y) \to (z \in y)$, it is obvious for $(\text {Eq II})$, while the proof is a little bit tricky for $(\text {Eq I})$.
The issue is that the above definition does not provide "left-substitutuvity"; in order to do this, we need a further axiom, that we will call Extensionality:
$\text {Ext I}) \: \ (x \subseteq y \land y \subseteq x) \to x=y$, or
$\text {Ext II}) \: \ (x \in z \land x=y) \to y \in z$.

Note: the proof that $(\text {Eq I})$ above implies substitutivity wrt the right argument may be found into: Abraham Robinson, On the Independence of the Axioms of Definiteness (Axiome Der Bestimmtheit), Jou Symb Log (1939) and it needs some more axioms of set theory.
We have to prove that $x \in z$ and $x=y$ imply $y \in z$.
Using either Pair or Power-set axioms we have that there is a set $t$ such that $x \in t$, and by $(\text {Eq I})$ we have that also $y \in t$.
Assume now that "right-substitutivity" does not hold, i.e. that $\exists r (r \in x \land r \notin y)$.
Applying Separation to $t$ in the form: $\exists w \forall z [z \in w \leftrightarrow (z \in t \land r \in z)]$, we have that there is the set $w$ of those $z$ of $t$ for which $r \in z$. But $x \in w$ and $.y \notin w$, contrary to $(\text {Eq I})$.
A: Even without Extensionality or any set theoretic axioms whatsoever, if we are working in a language where the only atomic relation is $\in$, we can still define a notion of equality which works as expected.
$$\textbf{Definition:} A\approx B \iff \forall x, [x\in A \iff x\in B]\land[A\in x \iff B\in x]$$
It's a matter of simple logic to prove that $\approx$ is at least an equivalence relation; it's reflexive, symmetric, and transitive. However, this relation also obeys the substitution property: for every formula $\phi(x,A)$ in the language of set theory, it does indeed hold that $A\approx B \implies \forall x, (\phi(x,A)\iff \phi(x,B))$. To prove this, you would perform an induction over the length of the formula $\phi$. The base case has $\phi$ being one of the atomic formulae, so $\phi$ must be of the form $x\in A$ or $A\in x$ or $x\in y$, where $x,y$ are some variables different from $A$. The proof of substitution in these cases follows immediately from the definition of $\approx$. In the inductive case, we assume substitution works for the formulae $\phi$ and $\psi$, and then prove that it also works for the formula $\neg\phi$, and $\phi\land\psi$, and so on for the other connectives and the quantifiers. The inductive step doesn't actually use the $\approx$ definition; once you have substitution on the atomic formulae, you get substitution on the entire language for free. This is a metatheorem about FOL itself, nowhere do we use Extensionality.
Now, if we already had equality, we could still carry out the above construction of $\approx$, and we would still prove the substitution property for all formulae expressible without equality, but we wouldn't necessarily prove $\forall A, \forall B, A=B\iff A\approx B$. It turns out that this axiom is equivalent to the seemingly weaker second order axiom that "$=$ is definable from $\in$". Indeed, suppose we have some formula $\phi(A,B)$ in the language $\{\in\}$ which defines equality via $\forall A, \forall B, \phi(A,B)\iff A=B$. Applying $\approx$ substitution gives $A\approx B \implies [\phi(A,B)\iff \phi(A,A)]$, but $A=A\implies\phi(A,A)$ thus we get $A\approx B\implies \phi(A,B)$ and therefore $A\approx B\implies A=B$. We already know $A=B\implies A\approx B$, so we conclude that $A=B \iff A\approx B$. This fact, that "$=$ is definable" implies "$\approx$ defines $=$", again does not use any set theory axioms. In particular, Extensionality is never assumed.
As a matter of fact, the axiom "$\approx$ defines $=$" is so weak that it doesn't even prove any theorems about membership. Indeed, the extension of the first order language $\{\in\}$, where we add equality and then assert the above axiom, is indistinguishable from an extension by definition, which is necessarily a conservative extension. The reason is because $\approx$ already obeys all the axioms for $=$, namely reflexivity, symmetry, transitivity, and substitution. In this sense, our axiom $\forall A,\forall B, A\approx B \iff A=B$ is a genuine definition. This is not the case for the axiom of Extensionality, which is not a conservative extension to FOL in the language of $\in$. The axiom of Extensionality is typically as expressed as one of the following equivalent expressions.
$$\begin{align}
\forall A, \forall B, &[\forall x, x\in A\iff x\in A]\implies [\forall X, A\in X \iff B\in X] \\
\forall A, \forall B, &[\forall x, x\in A\iff x\in A]\implies A\approx B\\
\forall A, \forall B, &[\forall x, x\in A\iff x\in A]\iff A\approx B
\end{align}$$
I typically define Extensionality to be the second of these: if two sets have the same members, then they are relationally indistinguishable (i.e. they are equal). That being said, the equivalence of the above three expressions is easily proven using only first order logic, without assuming any set theory axioms at all. Unlike the previous principle, the axiom of Extensionality cannot be considered as a definition, and it has nontrivial consequences for the universe of sets.
In the event that Extensionality fails, it can be extremely difficult to recover. As a simple example, it's possible that every set $A$ admits a "copy" set $B$, which has exactly the same elements but is nonetheless distinguishable. It's also possible that each set $A$ admits a "near copy" $B$, where every member of $A$ has a copy member in $B$, but nonetheless $A$ and $B$ are entirely disjoint. It's also possible that each set $A$ admits a "near near copy" $B$, where every member of $A$ admits a near copy member in $B$, but every member of $A$ is disjoint from every member of $B$. To understand Extensionality as a matter of definition, you'd have to account for infinitely many of these notions of what it means to be a copy, and collapse them all into a single equivalence relation. This isn't possible without a great deal of pre-existing set theoretic framework, which can be difficult (if not impossible) to establish without already assuming Extensionality a priori. It's in this way that Extensionality rules out a very large variety of phenomenon, and is in some sense a rather profound assumption.
