\[\exists X : X = X.\]
AX-ZF-EXT. Axiom of Extensionality.
For any $X$ and $Y$,
\[\forall x : x\in X\lrimp x\in Y \enspace\rimp\enspace X=Y.\]
AX-ZF-EMP. Axiom of Empty Set.
There exists a set $X$ such that
\[\forall x : x\notin X.\]
By Axiom of Extensionality, the set $X$ above is unique. We call it the empty set,
\[\varnothing.\]
AX-ZF-SEP. Separation Schema / Specification 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.
DEF-ZF-BLD. Set-Builder Notation.
By Axiom of Extensionality, the set $Y$ above is unique. We write
\[Y = \{x\in X : \varphi(x,p)\}.\]
AX-ZF-REP. 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 a function and $X$ is a set, then $F[X]$ is always a set.
For any $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, the set $X$ above is unique. We call it the pair of $a$ and $b$,
\[\{a,b\}.\]
The singleton $\{a\}$ is the set $\{a,a\}$.
For any $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, the set $Y$ above is unique. We call it the union of $X$,
\[\bigcup X.\]We write
\[A\cup B = \bigcup\{A,B\}.\]
$X$ is a subset of $Y$, written $X\subseteq Y$, if
\[\forall x :\enspace x\in X \enspace\rimp\enspace x\in Y.\]$X$ is a proper subset of $Y$, written $X\subset Y$, if $X\subseteq Y$ and $X\neq Y$.
For any $X$ there exists a set $Y$ such that
\[\forall y :\enspace y\in Y \enspace\lrimp\enspace y\subseteq X.\]
By Axiom of Extensionality, the set $Y$ above is unique. We call it the power set of $X$,
\[\powerset(X).\]
$X$ and $Y$ are called disjoint if
\[\forall x : \neg(x\in X\land x\in Y).\]
$X$ is called non-empty if
\[\exists x : x\in X.\]
AX-ZF-REG. Axiom of Regularity / Axiom of Foundation.
Every non-empty set $X$ has an element $x$ that is disjoint from $X$.
No set is an element of itself.
Proof.For any $X$, apply Axiom of Regularity to $\{X\}$.
There exists a set $X$ such that $\varnothing\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.
- 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, $\ZF$ technically only needs the following axioms:
- Replacement Schema.
- Axiom of Extensionality.
- Axiom of Pairing.
- Axiom of Union.
- Axiom of Power Set.
- Axiom of Regularity.
- Axiom of Infinity.