# Why isn’t this an axiom of choice?

The standard axiom of choice can be expressed in the first order language of ZF by $$forall Xbig((Xneqemptysetwedgeemptysetnotin X)impliesexists f:Xtobigcup X forall Yin X(f(Y)in Y)big).$$ Naively, a simpler version would seem to be $$forall X(Xneqemptysetimpliesexists f:{X}to X)$$ since we then have that $$forall Ain{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?