Consider the following equivalent statements:

~ (x) (...x...) (x) ~ (...x...)
(x) ~ (...x...) ~ (x) (...x...)
~ (x) ~ (...x...) (x) (...x...)
(x) (...x...) ~ ( x) ~ (...x...)

The quantifier-negation (QN) rule allows us to make substitutions in accordance with these equivalences.

A statement of the form ~ (x) (...x...), for example, can be replaced by (x) ~ (...x...).

Like an equivalence rule in propositional logic, QN can be applied either to a whole statement or to a part.