|Description: Axiom of Quantified
Negation. This axiom is used to manipulate negated
quantifiers. One of the 4 axioms of pure predicate calculus. Equivalent
to axiom scheme C7' in [Megill] p. 448 (p.
16 of the preprint). An
alternate axiomatization could use ax467 1752 in place of ax-4 1692,
and ax-7 1535.
This axiom is redundant, as shown by theorem ax6o 1696.
Normally, ax6o 1696 should be used rather than ax-6o 1697, except by theorems
specifically studying the latter's properties. (Contributed by NM,
5-Aug-1993.) (New usage is discouraged.)