I'm struggling to understand a remark in Daniel Leivant's Higher Order Logic (link), namely that in section 3.3 on page 16:
It is mentioned that any second-order formula can be brought into prenex normal form, which is indeed easy to see. However, then he says:
A second order prenex formula $\psi$ can be further transformed (without increasing the number of quantifiers in any kind) into an equivalent formula $\psi^*$ in which no second order quantifier falls in the scope of a first order quantifier.
He then describes a procedure on how to recursively move out second-order quantifiers, where the key part is:
replace $\forall x\exists f\; \phi[x,f]$ by $\exists g\forall x\; \phi[x,g_x]$ where $g_x(z) := g(x,z)$, ...
and similarly for quantifiers over relation variables. The formulas in above sentence are equivalent by a weak form of the Axiom of Choice
Now, I'm working in monadic second-order logic, so I only need to (and can) quantify over sets. I'm guessing the replacement would then look like: $$\forall x\exists A\; \phi[x,A]\text{ by }\exists B\forall x\;\phi[x,B_x],$$ but I do not see how I could formally make this $B_x$, since it looks like we need to define $B_x := B(x)$ (which would mean $B$ is no longer a set, but rather a function), or at least we need to define a pairing function $\langle\cdot,\cdot\rangle$ such that $y\in B_x\rightleftarrows \langle x,y\rangle\in B$, and in the domain I'm working in (finite words over $\{0,1\}$, with immediate successor functions and lexicographic ordering defined) this doesn't seem to be possible.
So now I'm wondering: does this method work in monadic second-order logic, i.e. how could we define $B$ or $B_x$, or is there another way to see we can indeed swap first-order quantifiers and monadic second-order quantifiers using some form of the axiom of choice?