Axiom ax-c7

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.)

	Ref	Expression
Assertion	ax-c7	$$⊢\neg \forall x\neg \forall x\phi \to \phi$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		wph	$$wff\phi$$
2	1 0	wal	$$wff\forall x\phi$$
3	2	wn	$$wff\neg \forall x\phi$$
4	3 0	wal	$$wff\forall x\neg \forall x\phi$$
5	4	wn	$$wff\neg \forall x\neg \forall x\phi$$
6	5 1	wi	$$wff\left(\neg \forall x\neg \forall x\phi \to \phi \right)$$