Editing Zermelo–Fraenkel set theory (section)

=== Axiom of extensionality ===
{{Main|Axiom of extensionality}}

Two sets are equal (are the same set) if they have the same elements.

<div style="margin-left:1.6em;"><math>\forall x \forall y [\forall z (z \in x \Leftrightarrow z \in y) \Rightarrow x = y].</math></div>

The converse of this axiom follows from the substitution property of [[equality (mathematics)|equality]]. ZFC is constructed in first-order logic. Some formulations of first-order logic include identity; others do not. If the variety of first-order logic in which one is constructing set theory does not include equality "<math>=</math>", <math>x=y</math> may be defined as an abbreviation for the following formula:<ref>{{harvnb|Hatcher|1982|p=138}}, def.&nbsp;1.</ref> <math>\forall z [z \in x \Leftrightarrow z \in y] \land \forall w [x \in w \Leftrightarrow y \in w].</math>

In this case, the axiom of extensionality can be reformulated as

<div style="margin-left:1.6em;"><math>\forall x \forall y [\forall z (z \in x \Leftrightarrow z \in y) \Rightarrow \forall w (x \in w \Leftrightarrow y \in w)],</math></div>

which says that if <math>x</math> and <math>y</math> have the same elements, then they belong to the same sets.{{sfn|Fraenkel|Bar-Hillel|Lévy|1973}}