# Metamath Proof Explorer

## 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 ¬ ∀ 𝑥 𝑥 = 𝑦