# axioms of equality

Every text I've come across uses the Axiom of Extensionality to describe the fact that sets are equal iff they contain each other's elements. $$(\forall x)(\forall y)\bigl((\forall a)(a\in x \iff a\in y) \implies (x=y)\bigr)$$ Some will regard this as an axiom, while some regard this as the very definition of equality (replacing the implication with a biconditional). Either way, the idea is that given two sets, regardless of how they were named, defined, or written, if they have exactly same elements, they are equal. A set can be described completely and only by its elements.

Another fun fact about sets is that equal sets are members of exactly the same collections. $$(\forall x)(\forall y)\bigl((x=y) \implies (\forall b)(x\in b \iff y\in b)\bigr)$$ I've always been comfortable with the idea that equal sets have the same elements, but the second fact is, to me at least, much more fascinating, and strikes a beautiful symmetry with the first.

If we choose to call the first fact the "Axiom of Extensionality" (which seems to be the convention), what is the name of the second fact? Is it another axiom, or can it be proven from the first? Are they logically equivalent? If we take Extensionality as a definition, then the second fact reduces to $$(\forall x)(\forall y)\bigl((\forall a)(a\in x \iff a\in y) \implies (\forall b)(x\in b \iff y\in b)\bigr)$$

Are there any texts that mention this? So far I have not seen it other than on Wikipedia.

• Quine was fond of taking the "axiom of extensionality" as the definition of "$=$", and adopting substitutivity/indiscernibility as an additional set theoretic axiom. But so far as I know he's just about the only author to arrange things this way. – Malice Vidrine Dec 15 '13 at 3:50

The second fact is a special case of the indiscernibility of identicals and is part of the definition of equality. The principle says, for all predicates $\phi (u, t_1, t_2, \ldots, t_n)$, $$\forall x . \forall y . (x = y) \to (\phi (x, t_1, t_2, \ldots, t_n) \leftrightarrow \phi (y, t_1, t_2, \ldots, t_n))$$ where $t_1, t_2, \ldots, t_n$ are arbitrary parameters. For the language of set theory in first-order logic without equality, the special case implies the general principle.
• The first axiom schema in the OP is an instance of identity of indiscernibles, because it asserts that if x, y "look the same" from the perspective of set containment (a \in x), then they are equal. Wikipedia has an entry on these two principles. – Ioannis Filippidis Jul 7 '17 at 22:00
1. $x=x$.
2. $x=y\rightarrow(\varphi\leftrightarrow\psi)$, where and $y$ is free for $x$ in $\varphi$ and $\psi$ is replacing some free variable $x$ by $y$ in $\varphi$.