Axiom ax-negf 330

Description: Axiom of quantified negation.

Assertion

Ref	Expression
ax-negf	⊦ (~ ∀x𝜑 ⊸ ∀x~ ∀x𝜑)

Detailed syntax breakdown of Axiom ax-negf

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff 𝜑
2		vx	. . . 4 var x
3	1, 2	wal 318	. . 3 wff ∀x𝜑
4	3	wneg 3	. 2 wff ~ ∀x𝜑
5	4, 2	wal 318	. 2 wff ∀x~ ∀x𝜑
6	4, 5	wli 61	1 wff (~ ∀x𝜑 ⊸ ∀x~ ∀x𝜑)

This axiom is referenced by: (None)