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 31985
 Description: Remove dependency on ax-13 2234 from dtru 4783. (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 31984 . . . . 5 𝑤 𝑥𝑤
2 ax-nul 4717 . . . . . 6 𝑧𝑥 ¬ 𝑥𝑧
3 sp 2041 . . . . . 6 (∀𝑥 ¬ 𝑥𝑧 → ¬ 𝑥𝑧)
42, 3eximii 1754 . . . . 5 𝑧 ¬ 𝑥𝑧
5 eeanv 2170 . . . . 5 (∃𝑤𝑧(𝑥𝑤 ∧ ¬ 𝑥𝑧) ↔ (∃𝑤 𝑥𝑤 ∧ ∃𝑧 ¬ 𝑥𝑧))
61, 4, 5mpbir2an 957 . . . 4 𝑤𝑧(𝑥𝑤 ∧ ¬ 𝑥𝑧)
7 ax9 1990 . . . . . . 7 (𝑤 = 𝑧 → (𝑥𝑤𝑥𝑧))
87com12 32 . . . . . 6 (𝑥𝑤 → (𝑤 = 𝑧𝑥𝑧))
98con3dimp 456 . . . . 5 ((𝑥𝑤 ∧ ¬ 𝑥𝑧) → ¬ 𝑤 = 𝑧)
1092eximi 1753 . . . 4 (∃𝑤𝑧(𝑥𝑤 ∧ ¬ 𝑥𝑧) → ∃𝑤𝑧 ¬ 𝑤 = 𝑧)
116, 10ax-mp 5 . . 3 𝑤𝑧 ¬ 𝑤 = 𝑧
12 equequ2 1940 . . . . . . 7 (𝑧 = 𝑦 → (𝑤 = 𝑧𝑤 = 𝑦))
1312notbid 307 . . . . . 6 (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 ↔ ¬ 𝑤 = 𝑦))
14 ax7 1930 . . . . . . . 8 (𝑥 = 𝑤 → (𝑥 = 𝑦𝑤 = 𝑦))
1514con3d 147 . . . . . . 7 (𝑥 = 𝑤 → (¬ 𝑤 = 𝑦 → ¬ 𝑥 = 𝑦))
1615bj-spimevv 31909 . . . . . 6 𝑤 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦)
1713, 16syl6bi 242 . . . . 5 (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦))
18 ax7 1930 . . . . . . . 8 (𝑥 = 𝑧 → (𝑥 = 𝑦𝑧 = 𝑦))
1918con3d 147 . . . . . . 7 (𝑥 = 𝑧 → (¬ 𝑧 = 𝑦 → ¬ 𝑥 = 𝑦))
2019bj-spimevv 31909 . . . . . 6 𝑧 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦)
2120a1d 25 . . . . 5 𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦))
2217, 21pm2.61i 175 . . . 4 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)
2322exlimivv 1847 . . 3 (∃𝑤𝑧 ¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)
2411, 23ax-mp 5 . 2 𝑥 ¬ 𝑥 = 𝑦
25 exnal 1744 . 2 (∃𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
2624, 25mpbi 219 1 ¬ ∀𝑥 𝑥 = 𝑦
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383  ∀wal 1473  ∃wex 1695 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-nul 4717  ax-pow 4769 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701 This theorem is referenced by:  bj-axc16b  31986  bj-eunex  31987  bj-dtrucor  31988  bj-dvdemo1  31990
 Copyright terms: Public domain W3C validator