Axiom ax-6o 2137

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 2169 in place of ax-4 2135, ax-6o 2137, and ax-7 1734.

This axiom is obsolete and should no longer be used. It is proved above as Theorem ax6o 1750. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)

Assertion

Ref	Expression
ax-6o	⊢ (¬ ∀x ¬ ∀xφ → φ)

Detailed syntax breakdown of Axiom ax-6o

Step	Hyp	Ref	Expression
1		wph	. . . . . 6 wff φ
2		vx	. . . . . 6 setvar x
3	1, 2	wal 1540	. . . . 5 wff ∀xφ
4	3	wn 3	. . . 4 wff ¬ ∀xφ
5	4, 2	wal 1540	. . 3 wff ∀x ¬ ∀xφ
6	5	wn 3	. 2 wff ¬ ∀x ¬ ∀xφ
7	6, 1	wi 4	1 wff (¬ ∀x ¬ ∀xφ → φ)

This axiom is referenced by:  ax6  2147  ax9from9o  2148  equid1  2158  ax46  2162  ax67  2165  ax467  2169  equid1ALT  2176