Why isn't this an axiom of choice?

Question

The standard axiom of choice can be expressed in the first order language of ZF by $$\forall X\big((X\neq\emptyset\wedge\emptyset\notin X)\implies\exists f:X\to\bigcup X\ \forall Y\in X(f(Y)\in Y)\big).$$ Naively, a simpler version would seem to be $$\forall X(X\neq\emptyset\implies\exists f:\{X\}\to X)$$ since we then have that $\forall A\in\{X\}(f(A)\in A)$, as specified explicitly in the choice axiom. This version is provable in ZF according to the discussion on this answer, however, and is thusly not an axiom of choice. How exactly do we lose choice moving from the first formulation to the second?

Answer 1

This is not the axiom of choice, since you're only requiring that given a single set, there is a function that selects an element from that set. It's just how we interpret quantifiers: first we replace $X$ with an instance, then we replace $f$ with an instance; but there's no requirement that these replacements are coherent.

Therefore, this is quite literally existential instantiation. This follows from the rules of logic, so it is provable in any weak theory you'd like (as long as you can discuss choice function in that theory).

If you switch the order of the quantifiers, $\exists f\forall X$, then you'd get something more akin to global choice, presuming you're working in second-order set theory.