Theorem dtru

Description: At least two sets exist (or in terms of first-order logic, the universe of discourse has two or more objects). Note that we may not substitute the same variable for both x and y (as indicated by the distinct variable requirement), for otherwise we would contradict stdpc6 .

This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext , ax-sep , or ax-pow . See dtruALT for a shorter proof using these axioms, and see dtruALT2 for a proof that uses ax-pow instead of ax-pr .

The proof makes use of dummy variables z and w which do not appear in the final theorem. They must be distinct from each other and from x and y . In other words, if we were to substitute x for z throughout the proof, the proof would fail. (Contributed by NM, 7-Nov-2006) Avoid ax-13 . (Revised by Gino Giotto, 5-Sep-2023) Avoid ax-12 . (Revised by Rohan Ridenour, 9-Oct-2024) Use ax-pr instead of ax-pow . (Revised by BTernaryTau, 3-Dec-2024)

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

Proof

Step	Hyp	Ref	Expression
1		el	$$⊢\exists wx\in w$$
2		ax-nul	$$⊢\exists z\forall x\neg x\in z$$
3		elequ1	$$⊢x=w\to \left(x\in z\leftrightarrow w\in z\right)$$
4	3	notbid	$$⊢x=w\to \left(\neg x\in z\leftrightarrow \neg w\in z\right)$$
5	4	spw	$$⊢\forall x\neg x\in z\to \neg x\in z$$
6	2 5	eximii	$$⊢\exists z\neg x\in z$$
7		exdistrv	$$⊢\exists w\exists z\left(x\in w\wedge \neg x\in z\right)\leftrightarrow \left(\exists wx\in w\wedge \exists z\neg x\in z\right)$$
8	1 6 7	mpbir2an	$$⊢\exists w\exists z\left(x\in w\wedge \neg x\in z\right)$$
9		ax9v2	$$⊢w=z\to \left(x\in w\to x\in z\right)$$
10	9	com12	$$⊢x\in w\to \left(w=z\to x\in z\right)$$
11	10	con3dimp	$$⊢\left(x\in w\wedge \neg x\in z\right)\to \neg w=z$$
12	11	2eximi	$$⊢\exists w\exists z\left(x\in w\wedge \neg x\in z\right)\to \exists w\exists z\neg w=z$$
13		equequ2	$$⊢z=y\to \left(w=z\leftrightarrow w=y\right)$$
14	13	notbid	$$⊢z=y\to \left(\neg w=z\leftrightarrow \neg w=y\right)$$
15		ax7v1	$$⊢x=w\to \left(x=y\to w=y\right)$$
16	15	con3d	$$⊢x=w\to \left(\neg w=y\to \neg x=y\right)$$
17	16	spimevw	$$⊢\neg w=y\to \exists x\neg x=y$$
18	14 17	syl6bi	$$⊢z=y\to \left(\neg w=z\to \exists x\neg x=y\right)$$
19		ax7v1	$$⊢x=z\to \left(x=y\to z=y\right)$$
20	19	con3d	$$⊢x=z\to \left(\neg z=y\to \neg x=y\right)$$
21	20	spimevw	$$⊢\neg z=y\to \exists x\neg x=y$$
22	21	a1d	$$⊢\neg z=y\to \left(\neg w=z\to \exists x\neg x=y\right)$$
23	18 22	pm2.61i	$$⊢\neg w=z\to \exists x\neg x=y$$
24	23	exlimivv	$$⊢\exists w\exists z\neg w=z\to \exists x\neg x=y$$
25	8 12 24	mp2b	$$⊢\exists x\neg x=y$$
26		exnal	$$⊢\exists x\neg x=y\leftrightarrow \neg \forall xx=y$$
27	25 26	mpbi	$$⊢\neg \forall xx=y$$