# Quantifiers,equivalence, scope and Skolemization

As I understand it, we basically have two ways of getting rid of existential quantifiers. The first one is to use the equivalence relation AxP is equivalent to ~Ex~P.
Can we use this relation, even though the existential quantifier is in the the scope of a universal quantifier? For instance, would Ax[H(x) -> EyG(x,y)] be equivalent to Ax[H(x) -> ~Ay~G(x,y)] ?

The other method is to use Skolemization. Why should be use Skolemization when we can just use the above equivalence relation?

If the existential quantifier is in the scope of a universal quantifier, we substitute the existential quantifier with a Skolem function, f, which takes as arguments all the variables bound by the universal quantifier. What do we do in the case when the existential quantifier appear before the universal quantifier? For instance Ex[P(x)->AyQ(y,x)]. Can we simply replace x with a constant, or do we need to substitute x=f(y)?

Thank you very much!