# 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!

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'. 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.