Even Z (without foundation) is enough to prove the standard equivalences of choice, e.g. AC iff Well-ordering Thm iff cardinal trichotomy iff surjective cardinal trichotomy.

I think it'd be better to use a different symbol then * since that's usually to convert a notion regarding injective cardinalities into surjective. Maybe + since you're strengthening the notion?

You could probably get a counterexample to the original question (with the usual foundation axiom) by starting with a ZFA model with a strongly amorphous set of atoms A and taking all the sets hereditarily a quotient of some $A^n,$ and reintroducing Foundation with the tricks in mathoverflow.net/a/314490/109573 or arxiv.org/abs/2312.11902

You’re right. I’ve rephrased it in terms of $[A]^{<\omega}.$

You’re more likely to get a positive answer here if you use surjective comparison $<^*$ instead.

See this post for the relationship between the fragments of choice and comprehension in second-order arithmetic: mathoverflow.net/questions/39201/…

Aren't your two formulations of a theory $T$ having DC equivalent? If DC is "true of $T,$" then $T$ proves $\phi$-DC by substituting $\psi(f, r):= (\forall g \exists s \phi(g, s)) \rightarrow \phi(f, r).$ This distinction only matters if we restrict DC to a fixed complexity of projective formulas, since $\psi$ has higher complexity than $\phi.$