The principle that every parameter free definable set admits a choice function has been found to be equivalent to full AC over the rest of axioms of ZF (see here)! However, I'll try here to present a version of this principle but in a different way, and the question is if the new presentation would also be haunted by a kind of the same argument in the original version.
Definable partition Choice: if $\phi$ is a formula in which only the symbol $``y"$ occurs free, then: $$\forall X: \\X=\{y \mid \phi\} \land \\\forall y \in X \, \forall z \in X \,(x \neq y \to y \cap z =\emptyset) \to \\\exists f (f:X \setminus \{\emptyset\} \to \bigcup X, \forall x \,(f(x) \in x))$$
In English: every parameter free definable family of pairwise disjoint sets, admits a choice function.
Is this principle also equivalent to AC, over the rest of axioms of ZF?
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.