This came up yesterday in my Real Analysis course. I´m not sure if it is the sort of thing you are looking for and I´m also not sure if the use of $AC$ is essential, but….
Suppose $X$ is a complete metric space and $\{E_n:n\in \omega\}$ is a nested sequence of non-empty closed subsets of $X$ such that $\lim_{n \to \infty} \operatorname{diam} (E_n)=0$. Then there is a point $p$ that belongs to every $E_n$.
The only proof I know of this uses countable choice to get a sequence $\{ x_n\}$ with $x_n \in E_n$; then this sequence is a Cauchy sequence, etc.
But then the object whose existence you are trying to prove (i.e. $p$) is unique, by the condition on the diameters.
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.
Best Answer
$2$-well ordered choice is enough to imply AC.
Let $α$ be any ordinal, and look at $\mathcal P^2(α)\setminus\{\emptyset\}$.
We have $x\in^2 \mathcal P^2(α)\setminus\{\emptyset\}⇒∃z⊆\mathcal P(α)\;(x\in z)⇒x\subseteq α⇒x\text{ is well orderable}$.
A choice function on $\mathcal P^2(α)\setminus\{\emptyset\}$ induce a well ordering on $\mathcal P(α)$.
"powerset of well-orderable set is well-orderable" is famously equivalent to the axiom of choice.