Axiom of Choice

DEF-AC-CF. Choice Function.

Let $X$ be a set of non-empty sets. A function $f$ is a choice function on $X$ if

\[\forall A\in X : f(A)\in A.\]

AX-AC. Axiom of Choice.

For any collection of non-empty sets $X$, there exists a choice function on $X$.

• Axiom of Choice is denoted by $\AC$.
• $\ZF+\AC$ is denoted by $\ZFC$.

PROP-AC-ZF.

$\AC$ is independent of $\ZF$.