Set Theory/Zermelo‒Fraenkel set theory

Definition (Zermelo‒Fraenkel set theory):

Zermelo‒Fraenkel set theory (ZF set theory) is the theory given by the following axioms (where most are written in the language of set theory ${\mathcal {L}}$):

1. Axiom of extensionality: $\forall x,y:(x=y)\Leftrightarrow \forall z:(z\in x\Leftrightarrow z\in y)$
2. Empty set: $\exists x:\forall y:(y\notin x)$
3. Pairing: $\forall x:\forall y:\exists m:\forall u:(u\in m)\Leftrightarrow ((u=x)\vee (u=y))$
4. Union: $\forall x:\exists u:\forall y:(y\in u)\Leftrightarrow (\exists z:(y\in z)\wedge (z\in x))$
5. Restricted comprehension schema: Given a set $y$ and a formula in the language of set theory $\phi (x)$. Then we have a set of all $z\in y$ such that $\phi (z)$ is true. We write this as the set $\{z\in y\,|\,\phi (z)\}$.
6. Replacement schema: Given a set $z$ and a formula in the language of set theory $\phi (x,y)$, such that for all $x$ there exists a unique $y$ such that $\phi (x,y)$ is true. Then there exists a set $a$ whose elements are all those $y$. We write this as the set $\{y\,|\,\exists x\in z:\phi (x,y)\}$.
7. Power set: $\forall x:\exists y:\forall z:(z\in y)\Leftrightarrow (\forall a:(a\in z)\Rightarrow (a\in x))$
8. Infinity: There exists an inductive set. An inductive set is one that contains an empty set, and if it contains $x$, then it contains $x\cup \{x\}$.

Note that in the Infinity axiom, we said that the inductive set contains `an' empty set. We will soon see that there is in fact a unique empty set, so we can change our definition of an inductive set to one that contains `the' empty set.