Axiom ax-dis 325

Description: Distinctness principle. When the value of 𝜑 is independent of x, a quantifier can be added.

Assertion

Ref	Expression
ax-dis	⊦ (𝜑 ⊸ ∀x𝜑)

Distinct variable group:   𝜑,x

Detailed syntax breakdown of Axiom ax-dis

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

This axiom is referenced by: (None)