Zermelo-Fraenkel Set Theory, denoted by $\ZF$, consists of the following axioms.
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.\]
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$.
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
\[Y = \{x \in X : \varphi(x, p)\}.\]
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 and $X$ is a set, then the image $F[X]$ is always a set.
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\}$.
For any set $a$, the singleton $\{a\}$ is the set $\{a, a\}$.
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 sets $A$ and $B$, we write
\[A \cup B = \bigcup \{A, B\}.\]
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.\]
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)$.
Two sets $X$ and $Y$ are disjoint if
\[\neg (\exists x : x \in X \land x \in Y).\]
Every non-empty set $X$ has an element $x$ that is disjoint from $X$.
As a corollary:
Proposition 1. Irreflexivity of $\in$.
No set is an element of itself.
Proof.βFor any set $X$, if $X \in X$, then $X$ and $\{X\}$ are not disjoint, contrary to Axiom of Regularity.
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$ such that $\empt \in X$.
- Axiom of Infinity implies Axiom of Existence and Axiom of Empty Set.
- Replacement Schema together with Axiom of Empty Set implies Separation Schema.
- Replacement Schema together with Axiom of Existence implies Axiom of Empty Set.
Therefore, the following axioms are enough to construct $\ZF$: