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 or ax-sep . See dtruALT for a shorter proof using these axioms.

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)

	Ref	Expression
Assertion	dtru	⊢ ¬ ∀ 𝑥 𝑥 = 𝑦

Proof

Step	Hyp	Ref	Expression
1		el	⊢ ∃ 𝑤 𝑥 ∈ 𝑤
2		ax-nul	⊢ ∃ 𝑧 ∀ 𝑥 ¬ 𝑥 ∈ 𝑧
3		sp	⊢ ( ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑧 )
4	2 3	eximii	⊢ ∃ 𝑧 ¬ 𝑥 ∈ 𝑧
5		exdistrv	⊢ ( ∃ 𝑤 ∃ 𝑧 ( 𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧 ) ↔ ( ∃ 𝑤 𝑥 ∈ 𝑤 ∧ ∃ 𝑧 ¬ 𝑥 ∈ 𝑧 ) )
6	1 4 5	mpbir2an	⊢ ∃ 𝑤 ∃ 𝑧 ( 𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧 )
7		ax9v2	⊢ ( 𝑤 = 𝑧 → ( 𝑥 ∈ 𝑤 → 𝑥 ∈ 𝑧 ) )
8	7	com12	⊢ ( 𝑥 ∈ 𝑤 → ( 𝑤 = 𝑧 → 𝑥 ∈ 𝑧 ) )
9	8	con3dimp	⊢ ( ( 𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧 ) → ¬ 𝑤 = 𝑧 )
10	9	2eximi	⊢ ( ∃ 𝑤 ∃ 𝑧 ( 𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧 ) → ∃ 𝑤 ∃ 𝑧 ¬ 𝑤 = 𝑧 )
11		equequ2	⊢ ( 𝑧 = 𝑦 → ( 𝑤 = 𝑧 ↔ 𝑤 = 𝑦 ) )
12	11	notbid	⊢ ( 𝑧 = 𝑦 → ( ¬ 𝑤 = 𝑧 ↔ ¬ 𝑤 = 𝑦 ) )
13		nfv	⊢ Ⅎ 𝑥 ¬ 𝑤 = 𝑦
14		ax7v1	⊢ ( 𝑥 = 𝑤 → ( 𝑥 = 𝑦 → 𝑤 = 𝑦 ) )
15	14	con3d	⊢ ( 𝑥 = 𝑤 → ( ¬ 𝑤 = 𝑦 → ¬ 𝑥 = 𝑦 ) )
16	13 15	spimefv	⊢ ( ¬ 𝑤 = 𝑦 → ∃ 𝑥 ¬ 𝑥 = 𝑦 )
17	12 16	syl6bi	⊢ ( 𝑧 = 𝑦 → ( ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) )
18		nfv	⊢ Ⅎ 𝑥 ¬ 𝑧 = 𝑦
19		ax7v1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 𝑦 → 𝑧 = 𝑦 ) )
20	19	con3d	⊢ ( 𝑥 = 𝑧 → ( ¬ 𝑧 = 𝑦 → ¬ 𝑥 = 𝑦 ) )
21	18 20	spimefv	⊢ ( ¬ 𝑧 = 𝑦 → ∃ 𝑥 ¬ 𝑥 = 𝑦 )
22	21	a1d	⊢ ( ¬ 𝑧 = 𝑦 → ( ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) )
23	17 22	pm2.61i	⊢ ( ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 )
24	23	exlimivv	⊢ ( ∃ 𝑤 ∃ 𝑧 ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 )
25	6 10 24	mp2b	⊢ ∃ 𝑥 ¬ 𝑥 = 𝑦
26		exnal	⊢ ( ∃ 𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀ 𝑥 𝑥 = 𝑦 )
27	25 26	mpbi	⊢ ¬ ∀ 𝑥 𝑥 = 𝑦