Description: Axiom of Quantified Negation. This axiom is used to manipulate negated
quantifiers. Equivalent to axiom scheme C7' in Megill p. 448 (p. 16 of
the preprint). An alternate axiomatization could use axc5c711 in place
of ax-c5 , ax-c7 , and ax-11 .

This axiom is obsolete and should no longer be used. It is proved above
as theorem axc7 . (Contributed by NM, 10-Jan-1993)(New usage is discouraged.)