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

Theorem axnulALT 5303
Description: Alternate proof of axnul 5304, proved from propositional calculus, ax-gen 1795, ax-4 1809, sp 2174, and ax-rep 5284. To check this, replace sp 2174 with the obsolete axiom ax-c5 38056 in the proof of axnulALT 5303 and type the Metamath program "MM> SHOW TRACE_BACK axnulALT / AXIOMS" command. (Contributed by Jeff Hoffman, 3-Feb-2008.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
axnulALT 𝑥𝑦 ¬ 𝑦𝑥
Distinct variable group:   𝑥,𝑦

Proof of Theorem axnulALT
Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax-rep 5284 . . 3 (∀𝑤𝑥𝑦(∀𝑥⊥ → 𝑦 = 𝑥) → ∃𝑥𝑦(𝑦𝑥 ↔ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥)))
2 sp 2174 . . . . . 6 (∀𝑥 ¬ ∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥) → ¬ ∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥))
32con2i 139 . . . . 5 (∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥) → ¬ ∀𝑥 ¬ ∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥))
4 df-ex 1780 . . . . 5 (∃𝑥𝑦(∀𝑥⊥ → 𝑦 = 𝑥) ↔ ¬ ∀𝑥 ¬ ∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥))
53, 4sylibr 233 . . . 4 (∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥) → ∃𝑥𝑦(∀𝑥⊥ → 𝑦 = 𝑥))
6 fal 1553 . . . . . 6 ¬ ⊥
7 sp 2174 . . . . . 6 (∀𝑥⊥ → ⊥)
86, 7mto 196 . . . . 5 ¬ ∀𝑥
98pm2.21i 119 . . . 4 (∀𝑥⊥ → 𝑦 = 𝑥)
105, 9mpg 1797 . . 3 𝑥𝑦(∀𝑥⊥ → 𝑦 = 𝑥)
111, 10mpg 1797 . 2 𝑥𝑦(𝑦𝑥 ↔ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥))
128intnan 485 . . . . . 6 ¬ (𝑤𝑧 ∧ ∀𝑥⊥)
1312nex 1800 . . . . 5 ¬ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥)
1413nbn 371 . . . 4 𝑦𝑥 ↔ (𝑦𝑥 ↔ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥)))
1514albii 1819 . . 3 (∀𝑦 ¬ 𝑦𝑥 ↔ ∀𝑦(𝑦𝑥 ↔ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥)))
1615exbii 1848 . 2 (∃𝑥𝑦 ¬ 𝑦𝑥 ↔ ∃𝑥𝑦(𝑦𝑥 ↔ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥)))
1711, 16mpbir 230 1 𝑥𝑦 ¬ 𝑦𝑥
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  wal 1537   = wceq 1539  wfal 1551  wex 1779  wcel 2104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-12 2169  ax-rep 5284
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-fal 1552  df-ex 1780
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator