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?
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:
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.:
These are the left-to-right directions of your conditions 1 and 2.
Now, it’s obvious that doing the following is equivalent:
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