The Axiom of Choice is stated on this page and assumed by no proof on it; the two statements that would need it are identified and left unsettled

The Axiom of Choice is stated on this page, at The Axiom of Choice, together with the notion of a choice function it is stated in terms of, Choice function. Nothing on the page assumes it: every proof here is carried out without any choice principle, and two natural-looking statements are missing from the page for exactly that reason. This is the account of where the line falls.

What is proved without choice, and why. A construction is choice-free when the object it produces is determined by the data rather than selected from several candidates. The two-sided inverse of $f : A \to B$ is a bijection if and only if there is a function $g : B \to A$ with $g \circ f = \Delta_A$ and $f \circ g = \Delta_B$; such a $g$ is unique, equals the inverse relation $f^{-1}$, and is itself a bijection is determined: for a bijection $f$ and a point $b$ of the codomain there is exactly one $a$ with $f(a) = b$, so no selection is made. The left inverse of For $f : A \to B$ with $A \neq \varnothing$: $f$ is injective if and only if there is $g : B \to A$ with $g \circ f = \Delta_A$; for $A = \varnothing$ the empty function is injective and has a left inverse if and only if $B = \varnothing$ needs one arbitrary point $a_{0}$ of a nonempty set, which is a single existential instantiation and not a choice principle: one point is chosen once, not one point for each index. The function produced by Let $\sim$ be an equivalence relation on $A$ with quotient map $\pi : A \to A/{\sim}$, and let $f : A \to B$. There is a function $g : A/{\sim} \to B$ with $g \circ \pi = f$ if and only if $a \sim a'$ implies $f(a) = f(a')$; and such a $g$ is then unique is likewise determined, because its value on a class is forced to be the common value of $f$ on that class, and The equivalence classes of an equivalence relation are nonempty, cover $A$, and are pairwise equal or disjoint; conversely every such cover arises from exactly one equivalence relation is proved from the three defining properties alone.

A choice function is an element of a product, and the two formulations of the axiom are one statement. The Axiom of Choice gives the axiom twice, once as "every family of nonempty sets has a choice function" and once as "a product of nonempty sets is nonempty", and both objects are now defined on this page, so the passage between the two readings can be written out. Let $\mathcal{F}$ be a set all of whose members are nonempty, and index it by itself: the identity relation $\Delta_{\mathcal{F}}$ of The identity relation $\Delta_A = \{\,(a,b) \in A \times A : a = b\,\}$ and the membership relation $\in_A\, = \{\,(a,b) \in A \times A : a \in b\,\}$ is a function with domain $\mathcal{F}$ sending each $S$ to itself, by clause (ii) of If $f$ and $g$ are functions then $g \circ f$ is a function with domain $f^{-1}[\operatorname{dom} g]$ and $(g \circ f)(x) = g(f(x))$ there; $\Delta_A$ is a function with $\Delta_A(a) = a$; and $f \circ \Delta_A = f = \Delta_B \circ f$ for $f : A \to B$, hence an indexed family (An indexed family $(A_i)_{i \in I}$ is a function with domain $I$; $\{A_i : i \in I\}$ is its range) whose range is $\mathcal{F}$, so its indexed union is $\bigcup \mathcal{F}$ ($\bigcup_{i \in I} A_i := \bigcup \{A_i : i \in I\}$, and $\bigcap_{i \in I} A_i := \bigcap \{A_i : i \in I\}$ for $I \neq \varnothing$). Unfolding The product $\prod_{i \in I} A_i := \{\, f : I \to \bigcup_{i \in I} A_i \ \mid\ f(i) \in A_i \text{ for every } i \in I \,\}$ for that family gives the set of functions $g : \mathcal{F} \to \bigcup \mathcal{F}$ with $g(S) \in S$ for every $S \in \mathcal{F}$, which is word for word the set of choice functions for $\mathcal{F}$ in Choice function. So a choice function for $\mathcal{F}$ is exactly an element of the product of the members of $\mathcal{F}$, and the two formulations assert the same thing about the same object.

The first statement that would need choice: a right inverse for a surjection. For a surjection $f : A \to B$ (Injection, surjection, bijection) each $b \in B$ has at least one preimage, and a right inverse is a rule picking one preimage for every $b$ at once. That is a simultaneous selection over the whole of $B$, and no proof on this page makes one: the assertion that every surjection has a right inverse is equivalent to the Axiom of Choice.

The second: a nonempty product. $\prod_{i \in \varnothing} A_i = \{\varnothing\}$; if $A_j = \varnothing$ for some $j \in I$ then $\prod_{i \in I} A_i = \varnothing$; and for $I = \{j\}$ the evaluation $f \mapsto f(j)$ is a bijection $\prod_{i \in I} A_i \to A_j$ settles $\prod_{i \in I} A_i$ when $I$ has no element, when some member is empty, and when $I$ has exactly one element, and For $I = \{\varnothing,\{\varnothing\}\}$ with $A_{\varnothing} = A$ and $A_{\{\varnothing\}} = B$, the map $f \mapsto (f(\varnothing), f(\{\varnothing\}))$ is a bijection $\prod_{i \in I} A_i \to A \times B$ settles the two-index case, in each case by writing an element down. For an arbitrary index set the assertion that $\prod_{i \in I} A_i$ is nonempty whenever every $A_i$ is nonempty is the product formulation of the axiom, which by the identification above is the choice-function formulation read at the family indexed by itself; The product $\prod_{i \in I} A_i := \{\, f : I \to \bigcup_{i \in I} A_i \ \mid\ f(i) \in A_i \text{ for every } i \in I \,\}$ says so where the product is introduced.

Where the rest of the library's account of choice lives. The strength of the weaker choice principles relative to one another, and what survives without any of them, is recorded at The choice ledger: what costs the Axiom of Choice and what does not ↗.