Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-dtru Structured version   Visualization version   GIF version

Theorem bj-dtru 34251
Description: Remove dependency on ax-13 2379 from dtru 5236. (Contributed by BJ, 31-May-2019.)

TODO: This predates the removal of ax-13 2379 in dtru 5236. But actually, sn-dtru 39398 is better than either, so move it to Main with sn-el 39397 (and determine whether bj-dtru 34251 should be kept as ALT or deleted).

(Proof modification is discouraged.) (New usage is discouraged.)

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

Proof of Theorem bj-dtru
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 el 5235 . . . . 5 𝑤 𝑥𝑤
2 ax-nul 5174 . . . . . 6 𝑧𝑥 ¬ 𝑥𝑧
3 sp 2180 . . . . . 6 (∀𝑥 ¬ 𝑥𝑧 → ¬ 𝑥𝑧)
42, 3eximii 1838 . . . . 5 𝑧 ¬ 𝑥𝑧
5 exdistrv 1956 . . . . 5 (∃𝑤𝑧(𝑥𝑤 ∧ ¬ 𝑥𝑧) ↔ (∃𝑤 𝑥𝑤 ∧ ∃𝑧 ¬ 𝑥𝑧))
61, 4, 5mpbir2an 710 . . . 4 𝑤𝑧(𝑥𝑤 ∧ ¬ 𝑥𝑧)
7 ax9 2125 . . . . . . 7 (𝑤 = 𝑧 → (𝑥𝑤𝑥𝑧))
87com12 32 . . . . . 6 (𝑥𝑤 → (𝑤 = 𝑧𝑥𝑧))
98con3dimp 412 . . . . 5 ((𝑥𝑤 ∧ ¬ 𝑥𝑧) → ¬ 𝑤 = 𝑧)
1092eximi 1837 . . . 4 (∃𝑤𝑧(𝑥𝑤 ∧ ¬ 𝑥𝑧) → ∃𝑤𝑧 ¬ 𝑤 = 𝑧)
116, 10ax-mp 5 . . 3 𝑤𝑧 ¬ 𝑤 = 𝑧
12 equequ2 2033 . . . . . . 7 (𝑧 = 𝑦 → (𝑤 = 𝑧𝑤 = 𝑦))
1312notbid 321 . . . . . 6 (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 ↔ ¬ 𝑤 = 𝑦))
14 ax7 2023 . . . . . . . 8 (𝑥 = 𝑤 → (𝑥 = 𝑦𝑤 = 𝑦))
1514con3d 155 . . . . . . 7 (𝑥 = 𝑤 → (¬ 𝑤 = 𝑦 → ¬ 𝑥 = 𝑦))
1615spimevw 2001 . . . . . 6 𝑤 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦)
1713, 16syl6bi 256 . . . . 5 (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦))
18 ax7 2023 . . . . . . . 8 (𝑥 = 𝑧 → (𝑥 = 𝑦𝑧 = 𝑦))
1918con3d 155 . . . . . . 7 (𝑥 = 𝑧 → (¬ 𝑧 = 𝑦 → ¬ 𝑥 = 𝑦))
2019spimevw 2001 . . . . . 6 𝑧 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦)
2120a1d 25 . . . . 5 𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦))
2217, 21pm2.61i 185 . . . 4 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)
2322exlimivv 1933 . . 3 (∃𝑤𝑧 ¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)
2411, 23ax-mp 5 . 2 𝑥 ¬ 𝑥 = 𝑦
25 exnal 1828 . 2 (∃𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
2624, 25mpbi 233 1 ¬ ∀𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  wal 1536  wex 1781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-nul 5174  ax-pow 5231
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator