Definition 1. A choice function on a set $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.
Proposition 1. $\AC$ is independent of $\ZF$.
Note. $\ZF + \AC$ is denoted by $\ZFC$.