Zermelo-Fraenkel Set Theory

Axiom 1. Axiom of Existence. There exists a set:

\[\exists X : X = X.\]

Axiom 2. Axiom of Extensionality. For any sets $X$ and $Y$,

\[(\forall x : x \in X \lrimp x \in Y) \enspace\rimp\enspace X = Y.\]

Axiom 3. Axiom of Empty Set. There exists a set $\empt$ such that

\[\forall x : x \notin \empt.\]

By Axiom of Extensionality, $\empt$ is unique and is called the empty set.

A set $Y$ is non-empty if $Y \neq \empt$.

Axiom 4. Separation Schema. Let $X$ be a set and $\varphi(x, p)$ be a formula with free variables among $x$ and $p$. For any $p$, there exists a set $Y$ such that

\[\forall x :\enspace% x \in Y \enspace\lrimp\enspace x \in X \land \varphi(x, p).\]

In other words, a subclass of a set is always a set.

By Axiom of Extensionality, $Y$ is unique. We write (Set-Builder Notation)

\[Y = \{x \in X : \varphi(x, p)\}.\]

Axiom 5. Replacement Schema. Let $X$ be a set and $\varphi(x, y, p)$ be a formula with free variables among $x$, $y$ and $p$, such that

\[\forall x, y, z :\enspace% \varphi(x, y) \land \varphi(x, z) \enspace\rimp\enspace y = z.\]

Then, for any $p$, there exists a set $Y$ such that

\[\forall y :\enspace% y \in Y \enspace\lrimp\enspace \exists x : x \in X \land \varphi(x, y, p).\]

In other words, if a class $F$ is functional, then for any set $X$, the image $F[X]$ is always a set.

Axiom 6. Axiom of Pairing. For any sets $a$ and $b$ there exists a set $X$ such that

\[\forall x :\enspace% x \in X \enspace\lrimp\enspace x = a \lor x = b.\]

By Axiom of Extensionality, $X$ is unique. We call it the pair of $a$ and $b$, denoted by $\{a, b\}$.

Definition 1. For any set $a$, the singleton $\{a\}$ is the set $\{a, a\}$.

Axiom 7. Axiom of Union. For any set $X$ there exists a set $Y$ such that

\[\forall y :\enspace% y \in Y \enspace\lrimp\enspace \exists x : x \in X \land y \in x.\]

By Axiom of Extensionality, $Y$ is unique. We call it the union of $X$, denoted by $\bigcup X$.

For any two sets $A$ and $B$, we write

\[A \cup B = \bigcup \{A, B\}.\]

Definition 2. A set $X$ is a subset of a set $Y$, written $X \subseteq Y$, if

\[\forall x :\enspace% x \in X \enspace\rimp\enspace x \in Y.\]

Axiom 8. Axiom of Power Set. For any set $X$ there exists a set $Y$ such that

\[\forall y :\enspace% y \in Y \enspace\lrimp\enspace y \subseteq X.\]

By Axiom of Extensionality, $Y$ is unique. We call it the power set of $X$, denoted by $\powerset(X)$.

Definition 3. Two sets $X$ and $Y$ are disjoint if

\[\neg (\exists x : x \in X \land x \in Y).\]

Axiom 9. Axiom of Regularity. Every non-empty set $X$ has an element $x$ that is disjoint from $X$.

Proposition 1. Irreflexivity of $\in$. No set is an element of itself.

Axiom 10. Axiom of Infinity. There exists a set $X$ such that $\empt \in X$ and

\[\forall x :\enspace x \in X \enspace\rimp\enspace x \cup \{x\} \in X.\]

In other words, there exists an inductive set $X$ with $\empt \in X$.