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

Theorem axnulALT 5199
Description: Alternate proof of axnul 5200, proved from propositional calculus, ax-gen 1787, ax-4 1801, sp 2172, and ax-rep 5181. To check this, replace sp 2172 with the obsolete axiom ax-c5 35899 in the proof of axnulALT 5199 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 5181 . . 3 (∀𝑤𝑥𝑦(∀𝑥⊥ → 𝑦 = 𝑥) → ∃𝑥𝑦(𝑦𝑥 ↔ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥)))
2 sp 2172 . . . . . 6 (∀𝑥 ¬ ∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥) → ¬ ∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥))
32con2i 141 . . . . 5 (∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥) → ¬ ∀𝑥 ¬ ∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥))
4 df-ex 1772 . . . . 5 (∃𝑥𝑦(∀𝑥⊥ → 𝑦 = 𝑥) ↔ ¬ ∀𝑥 ¬ ∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥))
53, 4sylibr 235 . . . 4 (∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥) → ∃𝑥𝑦(∀𝑥⊥ → 𝑦 = 𝑥))
6 fal 1542 . . . . . 6 ¬ ⊥
7 sp 2172 . . . . . 6 (∀𝑥⊥ → ⊥)
86, 7mto 198 . . . . 5 ¬ ∀𝑥
98pm2.21i 119 . . . 4 (∀𝑥⊥ → 𝑦 = 𝑥)
105, 9mpg 1789 . . 3 𝑥𝑦(∀𝑥⊥ → 𝑦 = 𝑥)
111, 10mpg 1789 . 2 𝑥𝑦(𝑦𝑥 ↔ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥))
128intnan 487 . . . . . 6 ¬ (𝑤𝑧 ∧ ∀𝑥⊥)
1312nex 1792 . . . . 5 ¬ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥)
1413nbn 374 . . . 4 𝑦𝑥 ↔ (𝑦𝑥 ↔ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥)))
1514albii 1811 . . 3 (∀𝑦 ¬ 𝑦𝑥 ↔ ∀𝑦(𝑦𝑥 ↔ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥)))
1615exbii 1839 . 2 (∃𝑥𝑦 ¬ 𝑦𝑥 ↔ ∃𝑥𝑦(𝑦𝑥 ↔ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥)))
1711, 16mpbir 232 1 𝑥𝑦 ¬ 𝑦𝑥
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wal 1526   = wceq 1528  wfal 1540  wex 1771  wcel 2105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-12 2167  ax-rep 5181
This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1531  df-fal 1541  df-ex 1772
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator