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

Theorem axnulALT 5201
Description: Alternate proof of axnul 5202, proved from propositional calculus, ax-gen 1792, ax-4 1806, sp 2177, and ax-rep 5183. To check this, replace sp 2177 with the obsolete axiom ax-c5 36013 in the proof of axnulALT 5201 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 5183 . . 3 (∀𝑤𝑥𝑦(∀𝑥⊥ → 𝑦 = 𝑥) → ∃𝑥𝑦(𝑦𝑥 ↔ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥)))
2 sp 2177 . . . . . 6 (∀𝑥 ¬ ∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥) → ¬ ∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥))
32con2i 141 . . . . 5 (∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥) → ¬ ∀𝑥 ¬ ∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥))
4 df-ex 1777 . . . . 5 (∃𝑥𝑦(∀𝑥⊥ → 𝑦 = 𝑥) ↔ ¬ ∀𝑥 ¬ ∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥))
53, 4sylibr 236 . . . 4 (∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥) → ∃𝑥𝑦(∀𝑥⊥ → 𝑦 = 𝑥))
6 fal 1547 . . . . . 6 ¬ ⊥
7 sp 2177 . . . . . 6 (∀𝑥⊥ → ⊥)
86, 7mto 199 . . . . 5 ¬ ∀𝑥
98pm2.21i 119 . . . 4 (∀𝑥⊥ → 𝑦 = 𝑥)
105, 9mpg 1794 . . 3 𝑥𝑦(∀𝑥⊥ → 𝑦 = 𝑥)
111, 10mpg 1794 . 2 𝑥𝑦(𝑦𝑥 ↔ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥))
128intnan 489 . . . . . 6 ¬ (𝑤𝑧 ∧ ∀𝑥⊥)
1312nex 1797 . . . . 5 ¬ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥)
1413nbn 375 . . . 4 𝑦𝑥 ↔ (𝑦𝑥 ↔ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥)))
1514albii 1816 . . 3 (∀𝑦 ¬ 𝑦𝑥 ↔ ∀𝑦(𝑦𝑥 ↔ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥)))
1615exbii 1844 . 2 (∃𝑥𝑦 ¬ 𝑦𝑥 ↔ ∃𝑥𝑦(𝑦𝑥 ↔ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥)))
1711, 16mpbir 233 1 𝑥𝑦 ¬ 𝑦𝑥
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  wal 1531   = wceq 1533  wfal 1545  wex 1776  wcel 2110
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-12 2172  ax-rep 5183
This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1536  df-fal 1546  df-ex 1777
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator