Theorem dtruALT2

Description: Alternate proof of dtru using ax-pr instead of ax-pow . (Contributed by Mario Carneiro, 31-Aug-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	dtruALT2	$$⊢\neg \forall xx=y$$

Proof

Step	Hyp	Ref	Expression
1		0inp0	$$⊢y=\varnothing \to \neg y=\left\{\varnothing \right\}$$
2		snex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
3		eqeq2	$$⊢x=\left\{\varnothing \right\}\to \left(y=x\leftrightarrow y=\left\{\varnothing \right\}\right)$$
4	3	notbid	$$⊢x=\left\{\varnothing \right\}\to \left(\neg y=x\leftrightarrow \neg y=\left\{\varnothing \right\}\right)$$
5	2 4	spcev	$$⊢\neg y=\left\{\varnothing \right\}\to \exists x\neg y=x$$
6	1 5	syl	$$⊢y=\varnothing \to \exists x\neg y=x$$
7		0ex	$$⊢\varnothing \in \mathrm{V}$$
8		eqeq2	$$⊢x=\varnothing \to \left(y=x\leftrightarrow y=\varnothing \right)$$
9	8	notbid	$$⊢x=\varnothing \to \left(\neg y=x\leftrightarrow \neg y=\varnothing \right)$$
10	7 9	spcev	$$⊢\neg y=\varnothing \to \exists x\neg y=x$$
11	6 10	pm2.61i	$$⊢\exists x\neg y=x$$
12		exnal	$$⊢\exists x\neg y=x\leftrightarrow \neg \forall xy=x$$
13		eqcom	$$⊢y=x\leftrightarrow x=y$$
14	13	albii	$$⊢\forall xy=x\leftrightarrow \forall xx=y$$
15	12 14	xchbinx	$$⊢\exists x\neg y=x\leftrightarrow \neg \forall xx=y$$
16	11 15	mpbi	$$⊢\neg \forall xx=y$$