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

Theorem dtru 5262
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 2026.

This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext 2790 or ax-sep 5194. See dtruALT 5279 for a shorter proof using these axioms.

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 2381. (Revised by Gino Giotto, 5-Sep-2023.)

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 5261 . . . 4 𝑤 𝑥𝑤
2 ax-nul 5201 . . . . 5 𝑧𝑥 ¬ 𝑥𝑧
3 sp 2172 . . . . 5 (∀𝑥 ¬ 𝑥𝑧 → ¬ 𝑥𝑧)
42, 3eximii 1828 . . . 4 𝑧 ¬ 𝑥𝑧
5 exdistrv 1947 . . . 4 (∃𝑤𝑧(𝑥𝑤 ∧ ¬ 𝑥𝑧) ↔ (∃𝑤 𝑥𝑤 ∧ ∃𝑧 ¬ 𝑥𝑧))
61, 4, 5mpbir2an 707 . . 3 𝑤𝑧(𝑥𝑤 ∧ ¬ 𝑥𝑧)
7 ax9v2 2118 . . . . . 6 (𝑤 = 𝑧 → (𝑥𝑤𝑥𝑧))
87com12 32 . . . . 5 (𝑥𝑤 → (𝑤 = 𝑧𝑥𝑧))
98con3dimp 409 . . . 4 ((𝑥𝑤 ∧ ¬ 𝑥𝑧) → ¬ 𝑤 = 𝑧)
1092eximi 1827 . . 3 (∃𝑤𝑧(𝑥𝑤 ∧ ¬ 𝑥𝑧) → ∃𝑤𝑧 ¬ 𝑤 = 𝑧)
11 equequ2 2024 . . . . . . 7 (𝑧 = 𝑦 → (𝑤 = 𝑧𝑤 = 𝑦))
1211notbid 319 . . . . . 6 (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 ↔ ¬ 𝑤 = 𝑦))
13 nfv 1906 . . . . . . 7 𝑥 ¬ 𝑤 = 𝑦
14 ax7v1 2008 . . . . . . . 8 (𝑥 = 𝑤 → (𝑥 = 𝑦𝑤 = 𝑦))
1514con3d 155 . . . . . . 7 (𝑥 = 𝑤 → (¬ 𝑤 = 𝑦 → ¬ 𝑥 = 𝑦))
1613, 15spimefv 2188 . . . . . 6 𝑤 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦)
1712, 16syl6bi 254 . . . . 5 (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦))
18 nfv 1906 . . . . . . 7 𝑥 ¬ 𝑧 = 𝑦
19 ax7v1 2008 . . . . . . . 8 (𝑥 = 𝑧 → (𝑥 = 𝑦𝑧 = 𝑦))
2019con3d 155 . . . . . . 7 (𝑥 = 𝑧 → (¬ 𝑧 = 𝑦 → ¬ 𝑥 = 𝑦))
2118, 20spimefv 2188 . . . . . 6 𝑧 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦)
2221a1d 25 . . . . 5 𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦))
2317, 22pm2.61i 183 . . . 4 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)
2423exlimivv 1924 . . 3 (∃𝑤𝑧 ¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)
256, 10, 24mp2b 10 . 2 𝑥 ¬ 𝑥 = 𝑦
26 exnal 1818 . 2 (∃𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
2725, 26mpbi 231 1 ¬ ∀𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wal 1526  wex 1771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-12 2167  ax-nul 5201  ax-pow 5257
This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1531  df-ex 1772  df-nf 1776
This theorem is referenced by:  dtrucor  5263  dvdemo1  5265  nfnid  5267  axc16b  5280  eunex  5281  brprcneu  6655  zfcndpow  10026
  Copyright terms: Public domain W3C validator