Theorem dtruALT

Description: Alternate proof of dtru which requires more axioms but is shorter and may be easier to understand. Like dtruALT2 , it uses ax-pow rather than ax-pr .

Assuming that ZF set theory is consistent, we cannot prove this theorem unless we specify that x and y be distinct. Specifically, Theorem spcev requires that x must not occur in the subexpression -. y = { (/) } in step 4 nor in the subexpression -. y = (/) in step 9. The proof verifier will require that x and y be in a distinct variable group to ensure this. You can check this by deleting the $d statement in set.mm and rerunning the verifier, which will print a detailed explanation of the distinct variable violation. (Contributed by NM, 15-Jul-1994) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		0inp0	$$⊢y=\varnothing \to \neg y=\left\{\varnothing \right\}$$
2		p0ex	$$⊢\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$$