Axiom ax-10 2019

Description: Axiom of Quantified Negation. Axiom C5-2 of [Monk2] p. 113. This axiom scheme is logically redundant (see ax10w 2006) but is used as an auxiliary axiom scheme to achieve scheme completeness. It means that 𝑥 is not free in ¬ ∀𝑥𝜑. (Contributed by NM, 21-May-2008.) Use its alias hbn1 2020 instead if you must use it. Any theorem in first order logic (FOL) that contains only set variables that are all mutually distinct, and has no wff variables, can be proved *without* using ax-10 2019 through ax-13 2246, by invoking ax10w 2006 through ax13w 2013. We encourage proving theorems *without* ax-10 2019 through ax-13 2246 and moving them up to the ax-4 1737 through ax-9 1999 section. (New usage is discouraged.)

Assertion

Ref	Expression
ax-10	⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)

Detailed syntax breakdown of Axiom ax-10

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff 𝜑
2		vx	. . . 4 setvar 𝑥
3	1, 2	wal 1481	. . 3 wff ∀𝑥𝜑
4	3	wn 3	. 2 wff ¬ ∀𝑥𝜑
5	4, 2	wal 1481	. 2 wff ∀𝑥 ¬ ∀𝑥𝜑
6	4, 5	wi 4	1 wff (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)

This axiom is referenced by:  hbn1  2020