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.
Best Answer
The second formula is an axiom of the first order logic with equality, together with the following axioms about equality:
Unlike Extensionality, which is a proper axiom, these equality axioms are valid in every normal models, hence they deserve the name "logical axioms".