Is Choice over definable sets equivalent to AC?

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?

Solution 1:

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.