The Axiom of Choice, sometimes abbreviated AC, is the following statement:
Axiom of Choice. For every set $Z$ whose members are disjoint nonempty sets, there exists a function $f$ whose domain is $Z$ and which maps every set in $Z$ to one of its elements. That is, for all $A\in Z$, $f(A)\in A$.
Here is an equivalent formulation:
For every set $Z$ whose members are disjoint nonempty sets, there exists a set $W$ such that $W\cap A = 1$ for all $A\in Z$.
Intuitively speaking, the Axiom of Choice states that it is always possible for us to make infinitely many arbitrary choices from a set of nonempty sets, in the same way that we may make a single arbitrary choice from a nonempty set (e.g. "since $A$ is nonempty, let $a$ be some element of $A$"). Here are two more formulations that are (nontrivially) equivalent to AC:
Axiom of Choice over Subsets. For every set $A$, there exists a function $f$ mapping each nonempty subset of $A$ to one of its elements. In other words, there is a function $f:2^A\backslash\varnothing \to A$ with $f(A')\in A'$ for all nonempty $A'\subset A$.
General Principle of Choice. For every set $Z$ whose members are nonempty sets (not necessarily disjoint), there exists a function $f$ whose domain is $Z$ and which maps every set in $Z$ to one of its elements.
Theorem 1. The Axiom of Choice, the Axiom of Choice over Subsets, and the General Principle of Choice are all equivalent to each other.
Proof. We will show that AC $\implies$ ACS $\implies$ GPC $\implies$ AC.
First, let AC be given. We will show that we can define a choice function on $2^A\backslash\varnothing$ for any set $A$. Consider the set This set is related to the power set $2^A$, except that it replaces the elements in each of the subsets of $A$ with ordered pairs $(a,A')$ coupling each element with the subset that contains it. This makes $Z$ is a set of disjoint sets, so by AC we may find a choice function $f:Z\to (A\times 2^A)$. Finally, if we define the functions $g:2^A\backslash\varnothing\to Z$ and $h:(A\times 2^A)\to A$ as follows: then it follows that the function $h\circ f\circ g: 2^A\backslash\varnothing \to A$ is a choice function on $2^A\backslash\varnothing$. Hence, AC $\implies$ ACS.
Now let ACS be given, and let $Z$ be a set of nonempty sets, not necessarily disjoint. Let $Y=\bigcup Z$ be the union of all sets in $Z$. Then $Z\subset 2^Y\backslash\varnothing$, meaning that we may use the choice function on $2^Y$ given to us by ACS to construct a choice function on $Z$. Specifically, if $f:2^Y\backslash\varnothing\to Y$ is a choice function, and $i:Z\to 2^Y\backslash\varnothing$ is the inclusion map, then $f\circ i:Z\to Y$ is a choice function on $Z$. Hence ACS $\implies$ GPC.
Finally, it is clear that GPC $\implies$ AC, since it is identical to AC except that it relaxes the requirement of sets being disjoint. Thus, we have that all $3$ formulations are equivalent. $\blacksquare$
The Axiom of Choice is also equivalent to each of the following:
Tarski's Theorem
Trichotomy