Is definable partition choice equivalent to axiom of choice over ZF?
Solution 1:
Yes.
If choice fails, let $\alpha$ be the least such that $V_\alpha$ cannot be well-ordered. This is definable without parameters, of course. Now consider the family $\{\{a\}\times a\mid a\subseteq V_\alpha\}$. Again, definable, since $\alpha$ was definable.
Easily, any two elements in the family are pairwise disjoint, so by definable partition choice, it admits a choice function. But this choice function translates to a choice function from $V_{\alpha+1}=\mathcal P(V_\alpha)$, which means that $V_\alpha$ can be well-ordered after all.