A, (X)(y)(W)B  Qwhere A is some set of formulae, where W is some sequence of quantifiers, where B is a formula that does not begin with a quantifier, and where  indicates that the signature involved is .
Then to achieve this proof task, it suffices to do the proof task
A, (X)(W)P' [(y')] Qwhere (y') indicates the signature formed from  by adding a new function symbol y', called a Skolem function, with arguments given by X, and where P' is P with each free instance of y replaced by y'.
This rule, called Skolemization (after the logician Thoralf Skolem) is justified in Chapter 8 of Theorem Proving and Algebra.
For example, given the proof task (where the variables range over integers)
(x)(y)(x + y = 0)  Q .it suffices to prove
(x)(x + y'(x) = 0) [(y')] Q .where y'(x) is the Skolem function (it is the negation function in this case). In many cases the Skolemized form is easier to use.
This rule can be applied repeatedly to eliminate all existential quantifiers from formulae to the left of the symbol.