MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dtru Structured version   Visualization version   GIF version

Theorem dtru 5358
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 𝑥 and 𝑦 (as indicated by the distinct variable requirement), for otherwise we would contradict stdpc6 2031.

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

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

Assertion
Ref Expression
dtru ¬ ∀𝑥 𝑥 = 𝑦
Distinct variable group:   𝑥,𝑦

Proof of Theorem dtru
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 el 5356 . . . 4 𝑤 𝑥𝑤
2 ax-nul 5229 . . . . 5 𝑧𝑥 ¬ 𝑥𝑧
3 elequ1 2113 . . . . . . 7 (𝑥 = 𝑤 → (𝑥𝑧𝑤𝑧))
43notbid 318 . . . . . 6 (𝑥 = 𝑤 → (¬ 𝑥𝑧 ↔ ¬ 𝑤𝑧))
54spw 2037 . . . . 5 (∀𝑥 ¬ 𝑥𝑧 → ¬ 𝑥𝑧)
62, 5eximii 1839 . . . 4 𝑧 ¬ 𝑥𝑧
7 exdistrv 1959 . . . 4 (∃𝑤𝑧(𝑥𝑤 ∧ ¬ 𝑥𝑧) ↔ (∃𝑤 𝑥𝑤 ∧ ∃𝑧 ¬ 𝑥𝑧))
81, 6, 7mpbir2an 708 . . 3 𝑤𝑧(𝑥𝑤 ∧ ¬ 𝑥𝑧)
9 ax9v2 2119 . . . . . 6 (𝑤 = 𝑧 → (𝑥𝑤𝑥𝑧))
109com12 32 . . . . 5 (𝑥𝑤 → (𝑤 = 𝑧𝑥𝑧))
1110con3dimp 409 . . . 4 ((𝑥𝑤 ∧ ¬ 𝑥𝑧) → ¬ 𝑤 = 𝑧)
12112eximi 1838 . . 3 (∃𝑤𝑧(𝑥𝑤 ∧ ¬ 𝑥𝑧) → ∃𝑤𝑧 ¬ 𝑤 = 𝑧)
13 equequ2 2029 . . . . . . 7 (𝑧 = 𝑦 → (𝑤 = 𝑧𝑤 = 𝑦))
1413notbid 318 . . . . . 6 (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 ↔ ¬ 𝑤 = 𝑦))
15 ax7v1 2013 . . . . . . . 8 (𝑥 = 𝑤 → (𝑥 = 𝑦𝑤 = 𝑦))
1615con3d 152 . . . . . . 7 (𝑥 = 𝑤 → (¬ 𝑤 = 𝑦 → ¬ 𝑥 = 𝑦))
1716spimevw 1998 . . . . . 6 𝑤 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦)
1814, 17syl6bi 252 . . . . 5 (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦))
19 ax7v1 2013 . . . . . . . 8 (𝑥 = 𝑧 → (𝑥 = 𝑦𝑧 = 𝑦))
2019con3d 152 . . . . . . 7 (𝑥 = 𝑧 → (¬ 𝑧 = 𝑦 → ¬ 𝑥 = 𝑦))
2120spimevw 1998 . . . . . 6 𝑧 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦)
2221a1d 25 . . . . 5 𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦))
2318, 22pm2.61i 182 . . . 4 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)
2423exlimivv 1935 . . 3 (∃𝑤𝑧 ¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)
258, 12, 24mp2b 10 . 2 𝑥 ¬ 𝑥 = 𝑦
26 exnal 1829 . 2 (∃𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
2725, 26mpbi 229 1 ¬ ∀𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wal 1537  wex 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-nul 5229  ax-pr 5351
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783
This theorem is referenced by:  brprcneu  6757  zfcndpow  10360
  Copyright terms: Public domain W3C validator