Axiom ax-L10 27

Description: Non-freeness of Negated Bound Variable.

Assertion

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

Detailed syntax breakdown of Axiom ax-L10

Step	Hyp	Ref	Expression
1		wff-ph	. . . 4 wff 𝜑
2		objvar-x	. . . 4 objvar 𝑥
3	1, 2	wff-forall 8	. . 3 wff ∀𝑥𝜑
4	3	wff-neg 9	. 2 wff ¬ ∀𝑥𝜑
5	4, 2	wff-forall 8	. 2 wff ∀𝑥 ¬ ∀𝑥𝜑
6	4, 5	wff-imp 10	1 wff (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)

This axiom is referenced by:  gennall-P6  730