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 32461
Description: Remove dependency on ax-13 2245 from dtru 4819. (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 32460 . . . . 5 𝑤 𝑥𝑤
2 ax-nul 4751 . . . . . 6 𝑧𝑥 ¬ 𝑥𝑧
3 sp 2051 . . . . . 6 (∀𝑥 ¬ 𝑥𝑧 → ¬ 𝑥𝑧)
42, 3eximii 1761 . . . . 5 𝑧 ¬ 𝑥𝑧
5 eeanv 2181 . . . . 5 (∃𝑤𝑧(𝑥𝑤 ∧ ¬ 𝑥𝑧) ↔ (∃𝑤 𝑥𝑤 ∧ ∃𝑧 ¬ 𝑥𝑧))
61, 4, 5mpbir2an 954 . . . 4 𝑤𝑧(𝑥𝑤 ∧ ¬ 𝑥𝑧)
7 ax9 2000 . . . . . . 7 (𝑤 = 𝑧 → (𝑥𝑤𝑥𝑧))
87com12 32 . . . . . 6 (𝑥𝑤 → (𝑤 = 𝑧𝑥𝑧))
98con3dimp 457 . . . . 5 ((𝑥𝑤 ∧ ¬ 𝑥𝑧) → ¬ 𝑤 = 𝑧)
1092eximi 1760 . . . 4 (∃𝑤𝑧(𝑥𝑤 ∧ ¬ 𝑥𝑧) → ∃𝑤𝑧 ¬ 𝑤 = 𝑧)
116, 10ax-mp 5 . . 3 𝑤𝑧 ¬ 𝑤 = 𝑧
12 equequ2 1950 . . . . . . 7 (𝑧 = 𝑦 → (𝑤 = 𝑧𝑤 = 𝑦))
1312notbid 308 . . . . . 6 (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 ↔ ¬ 𝑤 = 𝑦))
14 ax7 1940 . . . . . . . 8 (𝑥 = 𝑤 → (𝑥 = 𝑦𝑤 = 𝑦))
1514con3d 148 . . . . . . 7 (𝑥 = 𝑤 → (¬ 𝑤 = 𝑦 → ¬ 𝑥 = 𝑦))
1615bj-spimevv 32385 . . . . . 6 𝑤 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦)
1713, 16syl6bi 243 . . . . 5 (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦))
18 ax7 1940 . . . . . . . 8 (𝑥 = 𝑧 → (𝑥 = 𝑦𝑧 = 𝑦))
1918con3d 148 . . . . . . 7 (𝑥 = 𝑧 → (¬ 𝑧 = 𝑦 → ¬ 𝑥 = 𝑦))
2019bj-spimevv 32385 . . . . . 6 𝑧 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦)
2120a1d 25 . . . . 5 𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦))
2217, 21pm2.61i 176 . . . 4 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)
2322exlimivv 1857 . . 3 (∃𝑤𝑧 ¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)
2411, 23ax-mp 5 . 2 𝑥 ¬ 𝑥 = 𝑦
25 exnal 1751 . 2 (∃𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
2624, 25mpbi 220 1 ¬ ∀𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  wal 1478  wex 1701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-nul 4751  ax-pow 4805
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707
This theorem is referenced by:  bj-axc16b  32462  bj-eunex  32463  bj-dtrucor  32464  bj-dvdemo1  32466
  Copyright terms: Public domain W3C validator