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

Detailed syntax breakdown

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