Set Theory/Zermelo‒Fraenkel set theory

Definition (Zermelo‒Fraenkel set theory):

Zermelo‒Fraenkel set theory is the theory given by the following axioms:

1. Axiom of extensionality: $\forall x,y:x=y\Leftrightarrow (z\in x\Leftrightarrow z\in y)$
2. Empty set: $\exists \emptyset :\forall x:x\notin \emptyset$
3. Pairing:
4. Union:
5. Power set:
6. Regularity:
7. Infinity:
8. Comprehension: