Axiom ax-L6 18

Description: Axiom of Existence.

Note: '𝑥' cannot occur in '𝑡'

Assertion

Ref	Expression
ax-L6	⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑡

Distinct variable group:   𝑡,𝑥

Detailed syntax breakdown of Axiom ax-L6

Step	Hyp	Ref	Expression
1		objvar-x	. . . . . 6 objvar 𝑥
2	1	term-obj 1	. . . . 5 term 𝑥
3		term-t	. . . . 5 term 𝑡
4	2, 3	wff-equals 6	. . . 4 wff 𝑥 = 𝑡
5	4	wff-neg 9	. . 3 wff ¬ 𝑥 = 𝑡
6	5, 1	wff-forall 8	. 2 wff ∀𝑥 ¬ 𝑥 = 𝑡
7	6	wff-neg 9	1 wff ¬ ∀𝑥 ¬ 𝑥 = 𝑡

This axiom is referenced by:  axL6ex-P5  625