Is choice over definable sets equivalent to AC over axioms of ZF-Reg.? If we add the following axiom schema to ZF-Reg., 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, over axioms of ZF-Reg.?
The same question but over axioms of ZF was answered to the positive, and since ZF-Reg. is consistent with a  principle  stating that every class whose union is the universe won't be well-orderable, then this would kill the least fashioned argument used above.
It was noted that this matter is complicated, and that the answer might be to the negative, hence this question!
 A: Yes, indeed this kind of choice in general doesn't imply $\mathsf{AC}$ over $\mathsf{ZF}-\mathsf{Reg}$.
I will reason in $\mathsf{ZFC}$ and construct an interpretation of $\mathsf{ZF}-\mathsf{Reg}$, where $\mathsf{AC}$ fails, but choice for definable sets holds. The idea is to define a modified permutation model $M$ of $\mathsf{ZFU}+\lnot\mathsf{AC}$, where internally the collection of all urelements is a proper class and from external perspective any two urelements could be swapped by an automorphism. Definable choice holds in $M$, since due to the presence of automorphisms and the fact that urelements form a proper class, the only definable sets are sets whose transitive closure contains no urelements. Finally we convert $M$ to the desired model $M'$ of $(\mathsf{ZF}-\mathsf{Reg})$ by transforming each urelement $a$ into the set $\{a\}$.
Now let me outline the construction of $M$ in more details. We fix a countable set of urelements $U$ together with a function $r\colon U\to \mathbb{Q}$ such that $|r^{-1}(q)|=\aleph_0$, for all $q\in \mathbb{Q}$. We consider a group $G$ of permutations of $U$ consisting of all permutations $\pi\colon U\to U$ such that $r\circ \pi=r$. Let filter $\mathcal{F}$ on the lattice of subgroups of $G$ be generated by all the subgroups $\mathsf{Fix}_S=\{\pi\in G\mid \forall a\in S(\pi(a)=a)\}$, where $S$ is a finite subset of $U$.
We naturally define the universe $V_U$ of sets with urelements from $U$. Naturally we define the support function $\mathsf{supp}\colon V_U\to \mathcal{P}(U)$ and the action of $G$ on $V_U$. We say that  $x\in V_U$ is symmetric if $\{\pi \in G\mid \pi x= x\}\in \mathcal{F}$. And we say that $x\in V_U$ is hereditarily symmetric if it is symmetric and all elements of the transitive closure $\mathsf{TC}(x)$ are symmetric. We say that $x\in V_U$ is bounded if the set of rationals $r[\mathsf{supp}(x\cup\mathsf{TC}(x))]$ is bounded from above. The universe $M$ is a subuniverse of $V_U$ consisting of all $x\in V_U$ that are hereditarily symmetric and bounded.
Since $U$ itself isn't bounded, the urelements form a proper class in $M$. The proof that $M$ satisfies $\mathsf{ZFU}$ is essentially the standard proof that permutation models satisfy $\mathsf{ZFU}$. The proof that $M$ doesn't satisfy $\mathsf{AC}$ is also essentially standard: there are no well ordering of the set $r^{-1}(0)$, since otherwise we would be able to split $r^{-1}(0)$ into two disjoint infinite subsets and they wouldn't be symmetric. For any two $a,b\in A$ we easily find a permutaion $\sigma$ of $A$ such that $\sigma(a)=b$, $\sigma(b)=a$, $\forall c,d\in A(r(c)=r(d)\iff r(\sigma(c))=r(\sigma(d)))$, and for any $S\subseteq A$ the set $r[S]$ is bounded from above iff $r[\sigma[S]]$ is bounded from above. Obviously, such a permutation naturally extends to an automorphism of $M$ swapping $a$ with $b$.
Note that in fact I choose $M$ in such a manner that it satisfies even collection (and not merely replacement). Namely, consider the models $M_q\subseteq M$, for $q\in\mathbb{Q}$ that consist of all $x\in M$ such that $r[\mathsf{supp}(x)]$ is bounded from above by some $q'<q$. Clearly each $M_q$ is isomorphic to $M$ but furthermore $M_q$ is an elementary submodel to $M$, since we have isomorphisms fixing any given finite family of elements of $M_q$. Thus we always could find the result for an instance of collection as follows. We fix $q\in \mathbb{Q}$ such that all parameters used in this instance are from $M_q$. Then we find least $\alpha$ such that all desired witnesses could be found in $\alpha$-th level $V_U(\alpha)$ of $V_U$. And finally we observe that due to elementary submodel of $M$ and $M_q$ all the necessary witnesses could be found already in $V_U(\alpha)\cap M_q$, which in fact in fact is a bounded and hereditarily symmetric set.
