Recall the definition of [cardinal definable](https://mathoverflow.net/questions/412541/is-every-set-being-cardinal-definable-consistent-with-zf-negation-of-choice) sets, to re-iterate:


$Define: X \text { is cardinal definable} \iff \\\exists \text { cardinal } \kappa \, \exists \text { cardinals } \lambda\_1,.., \lambda\_n <^\rho \kappa \ \exists \phi : \\ X=\{ y \in V\_{\rho(\kappa)} \mid \phi^{V\_{\rho (\kappa)}} (y,\lambda\_1,..,\lambda\_n)\}$


Where: $\lambda\_i <^\rho \kappa \iff \rho(\lambda\_i) < \rho(\kappa)$, and $\rho$ is the rank function; and "*cardinal*" is defined after Scott's as an equivalence class under *bijection* of sets of the lowest possible rank.


That every set is cardinal definable is proved consistent with the failure of choice (see [here](https://mathoverflow.net/a/412591/95347)), on the other hand, it is also proved consistent with choice (see [here](https://mathoverflow.net/a/412536/95347)).



> 
> Now, working in $\sf ZF$, if we say that every cardinal definable set admits a choice function, would that entail full $\sf AC$?
> 
> 
> 



> 
> If we work in $\sf ZF-Reg.$, would cardinal definable choice imply $\sf AC$?
> 
> 
> 



Does cardinal definable choice imply AC?
Over ZF yes, it does.


Let $X$ be any family of nonempty sets, and let $κ$ be cardinal such that $ρ(κ)>ρ(X)$, then $V\_{ρ(κ)}\setminus\{∅\}$ is cardinal definable, hence has a choice function that induce a choice function on $X$.


In ZF-Regularity Scott trick doesn't work anymore, in fact Lévy has shown that it is consistent with ZF-Regularity that there is no assignment to each set a cardinality in any way (that is: it is consistent that there is no $C:V→V$ such that $C(x)=C(y)⇔|x|=|y|$ (even with parameters)).


In e.g. ZF-Regularity+AFA were you do have possible definition of cardinality for every set, similar idea to what I wrote above works: You start with with a set $X$, and define $X'=X\cap WF$ and $X^∘=X\setminus X'$, by the above $X'$ has a choice function, for $X^∘$ define $Y$ to be the class of accessible pointed graphs who are pictures for elements is in $Y$. Let $f:Y∩WF→X^∘$ be a function that sends $y$ to the unique element in $X^∘$ that $y$ is it's picture.


Note that $f''(Y∩WF)=X^∘$, and in fact that there exists a *set* $Z\subseteq Y∩WF$ such that $f''Z=X^∘$ (We don't need choice to get this $Z$, we can use Scott's trick, because $Y∩WF\subseteq WF$).


From the above $Z$ and $\bigcup Z$ are well-orderable, so let $x\in X^∘$, and $(G,E)∈Z$ be the minimal graph with the unique decoration $π$ such that $x\in\pi'' G$, and let $p$ be the minimal element (in $\bigcup Z$) such that such that $p E\pi^{-1}(x)$, and so $π(p)∈x$ and we have a choice function on $X=X'⊔X^∘$


