Does the Axiom of Choice give the strategy function for the existential quantifier in all formulas?

I was digging around the Axiom of Choice and looking at it from the angle that without choice, $\forall _{x\in S} \exists_{y\in\cup S} y\in x$ doesn't give us a function from the $x$ to the $y$, I found it obvious again and the situation without choice now looks ridiculous. Surely if the existential quantifier has a strategy, it should also exist in the object world of set theory.

I'm pretty sure choice can prove the existence of such a strategy for any claim of the form $\forall_{x\in X} \exists_{y\in Y} P(x,y)$ (in this answer J.D. Hamkins seems to say that the bounds on $y$ can be dropped, but I don't understand why). Now I am worried that the "ridiculous" situation arises even with choice in the case of more complicated forms. My intuition is that any true formula with bounded quantifiers in prenex form should imply the existence of a function describing the winning strategy for the existential quantifier. As far as I can tell, this even makes sense as an axiom schema of set theory. Has such an axiom schema been considered? Is it implied by $AC$? Is it at all (eqi)consistent with $ZF$?

Indeed, the construction of the strategy function generalizes to longer formulas. For completeness, for a formula $\forall_{x\in X}\exists_{y\in Y} R(x,y)$ where $R$ is a formula with two free variables, take the function $f:X\to 2^Y$ with $ f(x) =\{y \in Y : R(x,y)\}$ and compose it with a choice function for $2^Y$. This gives us $\exists_{g : X \to Y}\forall_{x\in X} R(x,g(x))$.

For a longer formula we can move the existential quantifiers to the left one by one. For example for $$\forall_{a\in A}\exists_{b\in B}\forall_{c\in C}\exists_{d\in D} S(a,b,c,d)$$ we can first take $$\forall_{a\in A}\exists_{b\in B} (\forall_{c\in C}\exists_{d\in D} S(a,b,c,d))$$ with the part in the parentheses being the $R$ from the two quantifier construction. We obtain $$\exists_{g : A \to B}\forall_{a\in A} \forall_{c\in C}\exists_{d\in D} S(a,b,c,d)$$ which can be rewritten as

$$\exists_{g : A \to B}\forall_{(a,c)\in A\times C}\exists_{d\in D} S(a,g(a),c,d)$$

then we can apply the construction again the part after the first existential quantifier.