If we add the following axiom schema to $\sf ZF$, would the resulting theory prove $\sf AC$?
Definable sets Choice: if $\phi$ is a formula in which only the symbol $“y"$ occurs free, then:
$$\forall X (X=\{y \mid \phi\} \to \\\exists f (f:X \setminus \{\emptyset\} \to \bigcup X \land \forall x (f(x) \in x)))$$
If not, then which form of choice this is equivalent to?
Best Answer
Yes, for the silliest reasons. First note that if $\alpha$ is definable without parameters, then so is its second power set, so the scheme implies that $2^\alpha$ can be well-ordered.
Next, note that the least $\alpha$ whose power set cannot be well-ordered is definable. Indeed, that is the definition.
So we get that the power set of every ordinal is well-orderable, and therefore choice holds. You can play this game using the $V_\alpha$S instead, if using the power sets of ordinals feels awkward.