Axiom ax-9d2

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

	Ref	Expression
Assertion	ax-9d2	⊢ ¬ ∀ 𝑥 ¬ 𝑥 = 𝑦

Detailed syntax breakdown

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