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](https://math.stackexchange.com/a/4314918/489784) to the positive, and since ZF-Reg. is consistent with a [principle](https://math.stackexchange.com/questions/4315049/is-it-consistent-with-sf-zf-fnd-that-no-class-whose-union-is-the-whole-univer?answertab=active#tab-top) 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](https://math.stackexchange.com/questions/4314897/is-choice-over-definable-sets-equivalent-to-ac?answertab=active#comment8991608_4314918) that this matter is complicated, and that the answer might be to the negative, hence this question!



Is choice over definable sets equivalent to AC over axioms of ZF-Reg.?
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.


