Axiom ax-9d2 33124

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

Assertion

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

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Axiom ax-9d2

Step	Hyp	Ref	Expression
1		vx	. . . . 5 setvar 𝑥
2		vy	. . . . 5 setvar 𝑦
3	1, 2	weq 1966	. . . 4 wff 𝑥 = 𝑦
4	3	wn 3	. . 3 wff ¬ 𝑥 = 𝑦
5	4, 1	wal 1537	. 2 wff ∀𝑥 ¬ 𝑥 = 𝑦
6	5	wn 3	1 wff ¬ ∀𝑥 ¬ 𝑥 = 𝑦

This axiom is referenced by: (None)