Skolemization is often used for eliminating existential quantifiers, which is often useful for proving theorems, especially in automated resolution theorem proving. Skolemization in first order predicate calculus is often based on a second order identity:

$\forall$x$\exists$y $\phi$(x,y) $\iff$ $\exists$f$\forall$x $\phi$(x, f(x))

I asked on the math.stackexchange site how to perform this operation in higher order logic, with a reasonably satisfactory answer, with one rather large caveat.

Apparently, at higher levels of logic, exploiting this identity to use an operation like Skolemization to eliminate existential quantifiers requires the axiom of choice. Is this always the case? This seems like a fairly heavy assumption for using a proof calculus, so are there any restricted forms of higher order Skolemization or existential quantifier elimination that don't require the axiom of choice, or require weaker versions of choice like countable choice or dependent choice?