Axiom ax-L5 17

Description: Axiom of Distinctness.

Note: '𝑥' cannot occur in '𝜑'.

Assertion

Ref	Expression
ax-L5	⊢ (𝜑 → ∀𝑥𝜑)

Distinct variable group:   𝜑,𝑥

Detailed syntax breakdown of Axiom ax-L5

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

This axiom is referenced by:  axL5ex-P5  613  allicv-P5  614  qimeqallav-P5-L1  617  qimeqallbv-P5-L1  619  qremallv-P5  656  cbvallv-P5-L1  658  lemma-L5.04a  667  genallw-P6  676  genexw-P6  677  nfrv-P6  686