ax-9d1 - Mathbox for Mario Carneiro

	Mathbox for Mario Carneiro		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ax-9d1		Structured version Visualization version GIF version

Axiom ax-9d1 33123

Description: Distinct variable version of ax-6 1971, equal variables case. (Contributed by Mario Carneiro, 14-Aug-2015.)

**Assertion**
Ref	Expression
ax-9d1	⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑥

**Detailed syntax breakdown of Axiom ax-9d1**
Step	Hyp	Ref	Expression
1		vx	. . . . 5 setvar 𝑥
2	1, 1	weq 1966	. . . 4 wff 𝑥 = 𝑥
3	2	wn 3	. . 3 wff ¬ 𝑥 = 𝑥
4	3, 1	wal 1537	. 2 wff ∀𝑥 ¬ 𝑥 = 𝑥
5	4	wn 3	1 wff ¬ ∀𝑥 ¬ 𝑥 = 𝑥

Colors of variables: wff setvar class

This axiom is referenced by: (None)