AX-ZF-EXT. Axiom of Extensionality.
For any $X$ and $Y$,
\[\forall x : x\in X\Leftrightarrow x\in Y \enspace\Rightarrow\enspace X=Y.\]
AX-ZF-EMP. Axiom of Empty Set.
There exists a set $X$ such that
\[\forall x : x\notin X.\]
DEF-ZF-EMP. Empty Set.
By Axiom of Extensionality, the set $X$ above is unique. We call it the empty set and write
\[X = \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\Leftrightarrow\enspace x\in X\land\varphi(x,p).\]
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\Rightarrow\enspace y=z.\]For any $p$, there exists a set $Y$ such that
\[\forall y :\enspace y\in Y \enspace\Leftrightarrow\enspace \exists x:x\in X\land\varphi(x,y,p).\]
AX-ZF-PR. Axiom of Pairing.
For any $a$ and $b$ there exists a set $X$ such that
\[\forall x :\enspace x\in X \enspace\Leftrightarrow\enspace x=a\lor x=b.\]
DEF-ZF-PR. Pair.
By Axiom of Extensionality, the set $X$ above is unique. We call it the pair of $a$ and $b$, and write
\[X = \{a,b\}.\]
DEF-ZF-SG. Singleton.
The singleton containing $a$, written as $\{a\}$, is the set $\{a,a\}$.
AX-ZF-U. Axiom of Union.
For any $X$ there exists a set $Y$ such that
\[\forall y :\enspace y\in Y \enspace\Leftrightarrow\enspace \exists x:x\in X\land y\in x.\]
DEF-ZF-U. Union.
By Axiom of Extensionality, $Y$ is unique. We call it the union of $X$ and write
\[Y = \bigcup X.\]For any $A$ and $B$, we define the union of $A$ and $B$ as
\[A\cup B = \bigcup\{A,B\}.\]
DEF-ZF-SUB. Subset.
$X$ is a subset of $Y$, written $X\subseteq Y$, if
\[\forall x :\enspace x\in X \enspace\Rightarrow\enspace x\in Y.\]$X$ is a proper subset of $Y$, written $X\subset Y$, if $X\subseteq Y$ and $X\neq Y$.
AX-ZF-P. Axiom of Power Set.
For any $X$ there exists a set $Y$ such that
\[\forall y :\enspace y\in Y \enspace\Leftrightarrow\enspace y\subseteq X.\]
DEF-ZF-P. Power Set.
By Axiom of Extensionality, the set $Y$ above is unique. We call it the power set of $X$ and write
\[Y = \mathcal{P}(X).\]
DEF-ZF-DJ. Disjoint Sets.
$X$ and $Y$ are called disjoint if
\[\forall x : \neg(x\in X\land x\in Y).\]
DEF-ZF-NEMP. Non-Empty Set.
$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$.
PROP-ZF-SLF.
No set is an element of itself.
Proof.Let $X$ be a set. Apply Axiom of Regularity to $\{X\}$.$\square$
AX-ZF-INF. Axiom of Infinity.
There exists a set $X$ such that $\varnothing\in X$ and
\[\forall x :\enspace x\in X \enspace\Rightarrow\enspace x\cup\{x\}\in X.\]
REM-ZF.
- Axiom of Infinity implies Axiom of Empty Set.
- Axiom of Replacement together with Axiom of Empty Set implies Axiom of Separation.