Well-ordering theorem

Every set admits a well-order. In ZF this statement is equivalent to the axiom of choice.

Given a choice function on all nonempty subsets of $X$, recursively choose the next point from the complement of all earlier choices. Hartogs theorem forces the recursion to exhaust $X$ before it defines an injection from $h(X)$ into $X$, producing a bijection from an ordinal to $X$.