Let $X$ be a non-empty set. A choice function on $X$ is a function on $X$ such that
\[\forall A \in X : f(A) \in A.\]
Axiom 1. Axiom of Choice ($\AC$).
Every set has a choice function.
$\AC$ is independent of $\ZF$.
Note. $\ZF + \AC$ is denoted by $\ZFC$.