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	$$⊢\neg \forall x\neg x=y$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1	0	cv	$$setvarx$$
2		vy	$$setvary$$
3	2	cv	$$setvary$$
4	1 3	wceq	$$wffx=y$$
5	4	wn	$$wff\neg x=y$$
6	5 0	wal	$$wff\forall x\neg x=y$$
7	6	wn	$$wff\neg \forall x\neg x=y$$