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

Theorem axnulALT 5172
Description: Alternate proof of axnul 5173, proved from propositional calculus, ax-gen 1802, ax-4 1816, sp 2184, and ax-rep 5154. To check this, replace sp 2184 with the obsolete axiom ax-c5 36520 in the proof of axnulALT 5172 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 5154 . . 3 (∀𝑤𝑥𝑦(∀𝑥⊥ → 𝑦 = 𝑥) → ∃𝑥𝑦(𝑦𝑥 ↔ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥)))
2 sp 2184 . . . . . 6 (∀𝑥 ¬ ∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥) → ¬ ∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥))
32con2i 141 . . . . 5 (∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥) → ¬ ∀𝑥 ¬ ∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥))
4 df-ex 1787 . . . . 5 (∃𝑥𝑦(∀𝑥⊥ → 𝑦 = 𝑥) ↔ ¬ ∀𝑥 ¬ ∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥))
53, 4sylibr 237 . . . 4 (∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥) → ∃𝑥𝑦(∀𝑥⊥ → 𝑦 = 𝑥))
6 fal 1556 . . . . . 6 ¬ ⊥
7 sp 2184 . . . . . 6 (∀𝑥⊥ → ⊥)
86, 7mto 200 . . . . 5 ¬ ∀𝑥
98pm2.21i 119 . . . 4 (∀𝑥⊥ → 𝑦 = 𝑥)
105, 9mpg 1804 . . 3 𝑥𝑦(∀𝑥⊥ → 𝑦 = 𝑥)
111, 10mpg 1804 . 2 𝑥𝑦(𝑦𝑥 ↔ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥))
128intnan 490 . . . . . 6 ¬ (𝑤𝑧 ∧ ∀𝑥⊥)
1312nex 1807 . . . . 5 ¬ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥)
1413nbn 376 . . . 4 𝑦𝑥 ↔ (𝑦𝑥 ↔ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥)))
1514albii 1826 . . 3 (∀𝑦 ¬ 𝑦𝑥 ↔ ∀𝑦(𝑦𝑥 ↔ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥)))
1615exbii 1854 . 2 (∃𝑥𝑦 ¬ 𝑦𝑥 ↔ ∃𝑥𝑦(𝑦𝑥 ↔ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥)))
1711, 16mpbir 234 1 𝑥𝑦 ¬ 𝑦𝑥
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wal 1540   = wceq 1542  wfal 1554  wex 1786  wcel 2114
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-12 2179  ax-rep 5154
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-fal 1555  df-ex 1787
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator