Axiom ax-9d1

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1	0	cv	⊢ 𝑥
2	1 1	wceq	⊢ 𝑥 = 𝑥
3	2	wn	⊢ ¬ 𝑥 = 𝑥
4	3 0	wal	⊢ ∀ 𝑥 ¬ 𝑥 = 𝑥
5	4	wn	⊢ ¬ ∀ 𝑥 ¬ 𝑥 = 𝑥