Different axiomatizations of set equality I've seen two definitions (or axioms?) of set equality:


*

*$a=b \Leftrightarrow (\forall x : x \in a \Leftrightarrow x \in b)$

*$a=b \Leftrightarrow (\forall x : a \in x \Leftrightarrow b \in x)$


That is, two sets are considered equal, if


*

*They contain the same sets

*They are contained in the same sets


ZFC seems to include the first version.
My question is: what is the connection between these? Does one follow from another?
I suspect the first version to be an axiom of (any) set theory, while the second is a consequence of first-order axioms for equality, like $a=b \Leftrightarrow [\phi(a) \leftrightarrow \phi(b)]$. In this case, why we need a special axiom in set theory? Doesn't it follow from equality axioms?
 A: The equality axioms of first-order logic are $a=b \Rightarrow [\phi(a) \Leftrightarrow \phi(b)]$, not $a=b \Leftrightarrow [\phi(a) \Leftrightarrow \phi(b)]$.  So only the $\Rightarrow$ direction of (1) and (2) follows from general first order-logic, whereas the $\Leftarrow$ direction has real content specific to set theory.  I've never seen (2) actually stated as an axiom of set theory.  However, it follows from the usual axioms of set theory.  For instance, Pairing says that for any $a$, there exists a set $x$ such that for all $c$, $c\in x \Leftrightarrow (c=a\vee c=a)$.  If $a\in x\Leftrightarrow b\in x$, plugging in the $x$ obtained from Pairing above gives that $b\in x$ and hence $b=a$.  This gives the $\Leftarrow$ direction of (2); as mentioned before, the $\Rightarrow$ direction is just part of first-order logic and has nothing to do with set theory in particular.
Note, however, that (2) does not imply (1), even in the presence of all the other axioms of set theory (and thus by symmetry, (1) does not imply (2) without assuming any additional axioms).  Indeed, (2) follows from Pairing and no other axioms, so any model of all the axioms of set theory except (1) will still satisfy (2).
A: The situation is rather simple at a higher level of abstraction.  We are interested here in a collection of objects U, equipped with some binary relation $\prec$, from which we can define two equivalence relations on U:


*

*$b_0\simeq b_1$ iff $\forall a, a \prec b_0 \iff a \prec b_1$;

*$a_0\backsimeq a_1$ iff $\forall b, a_0 \prec b \iff a_1 \prec b$.


An equality on U must be an equivalence relation $=$ for which all formulae all stable under substitution of equals by equals.  In general, we would require that all operations preserve the equality and all relations are invariant under it.  Here, we just need $\prec$ to be invariant under $=$, i.e.:


*

*$b_0 = b_1 \Longrightarrow b_0 \simeq b_1$;

*$a_0 = a_1 \Longrightarrow a_0 \backsimeq a_1$.


These are the left-to-right directions of your conditions 1 and 2.
Now, it’s obvious that doing the following is equivalent:


*

*Start from $U$, $\prec$ and an equality $=$ (satisfying 1 and 2), and require that $=$ coincides with $\simeq$ (i.e. the reverse of 1 holds).

*Start from $U$, $\prec$, define $=$ to be $\simeq$ (so that 1 and its reverse hold) and, to ensure that it is a proper equality, require condition 2.


Most often, people do the first and call the reverse of 1 (or the equivalence) the Axiom of Extensionality; some (like Takeuti and Zaring in Introduction to Axiomatic Set Theory, pp. 7-8 or Schechter in Handbook of Analysis and its Foundations, p. 29) do the second and call 2 the Axiom of Extensionality.
As Eric Wofsey mentions, the reverse of 2 holds if singletons exist, i.e. if for any $a$, there is a $b$ such that $x \prec b$ iff $x = a$:  we apply the definition of $a_0 \backsimeq a_1$ to that singleton $b$ obtained from $a_0$ (or $a_1$).  If we add everywhere the assumption of the existence of singletons, the two approaches above are thus also equivalent to


*

*Start from $U$, $\prec$, define $=$ to be $\backsimeq$ (so that 2 and its reverse hold), and require 1 and its reverse.

