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 33125
Description: Remove dependency on ax-13 2391 from dtru 5006. (Contributed by BJ, 31-May-2019.) (Proof modification 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 bj-el 33124 . . . . 5 𝑤 𝑥𝑤
2 ax-nul 4941 . . . . . 6 𝑧𝑥 ¬ 𝑥𝑧
3 sp 2200 . . . . . 6 (∀𝑥 ¬ 𝑥𝑧 → ¬ 𝑥𝑧)
42, 3eximii 1913 . . . . 5 𝑧 ¬ 𝑥𝑧
5 eeanv 2327 . . . . 5 (∃𝑤𝑧(𝑥𝑤 ∧ ¬ 𝑥𝑧) ↔ (∃𝑤 𝑥𝑤 ∧ ∃𝑧 ¬ 𝑥𝑧))
61, 4, 5mpbir2an 993 . . . 4 𝑤𝑧(𝑥𝑤 ∧ ¬ 𝑥𝑧)
7 ax9 2152 . . . . . . 7 (𝑤 = 𝑧 → (𝑥𝑤𝑥𝑧))
87com12 32 . . . . . 6 (𝑥𝑤 → (𝑤 = 𝑧𝑥𝑧))
98con3dimp 456 . . . . 5 ((𝑥𝑤 ∧ ¬ 𝑥𝑧) → ¬ 𝑤 = 𝑧)
1092eximi 1912 . . . 4 (∃𝑤𝑧(𝑥𝑤 ∧ ¬ 𝑥𝑧) → ∃𝑤𝑧 ¬ 𝑤 = 𝑧)
116, 10ax-mp 5 . . 3 𝑤𝑧 ¬ 𝑤 = 𝑧
12 equequ2 2108 . . . . . . 7 (𝑧 = 𝑦 → (𝑤 = 𝑧𝑤 = 𝑦))
1312notbid 307 . . . . . 6 (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 ↔ ¬ 𝑤 = 𝑦))
14 ax7 2098 . . . . . . . 8 (𝑥 = 𝑤 → (𝑥 = 𝑦𝑤 = 𝑦))
1514con3d 148 . . . . . . 7 (𝑥 = 𝑤 → (¬ 𝑤 = 𝑦 → ¬ 𝑥 = 𝑦))
1615bj-spimevv 33050 . . . . . 6 𝑤 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦)
1713, 16syl6bi 243 . . . . 5 (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦))
18 ax7 2098 . . . . . . . 8 (𝑥 = 𝑧 → (𝑥 = 𝑦𝑧 = 𝑦))
1918con3d 148 . . . . . . 7 (𝑥 = 𝑧 → (¬ 𝑧 = 𝑦 → ¬ 𝑥 = 𝑦))
2019bj-spimevv 33050 . . . . . 6 𝑧 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦)
2120a1d 25 . . . . 5 𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦))
2217, 21pm2.61i 176 . . . 4 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)
2322exlimivv 2009 . . 3 (∃𝑤𝑧 ¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)
2411, 23ax-mp 5 . 2 𝑥 ¬ 𝑥 = 𝑦
25 exnal 1903 . 2 (∃𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
2624, 25mpbi 220 1 ¬ ∀𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383  wal 1630  wex 1853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-nul 4941  ax-pow 4992
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859
This theorem is referenced by:  bj-axc16b  33126  bj-eunex  33127  bj-dtrucor  33128  bj-dvdemo1  33130
  Copyright terms: Public domain W3C validator