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

Theorem axnulALT 4710
Description: Alternate proof of axnul 4711, proved directly from ax-rep 4694 using none of the equality axioms ax-7 1922 through ax-c14 32988 provided we accept sp 2041 as an axiom. Replace sp 2041 with the obsolete ax-c5 32980 to see this in 'show traceback'. (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 4694 . . 3 (∀𝑤𝑥𝑦(∀𝑥⊥ → 𝑦 = 𝑥) → ∃𝑥𝑦(𝑦𝑥 ↔ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥)))
2 sp 2041 . . . . . 6 (∀𝑥 ¬ ∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥) → ¬ ∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥))
32con2i 133 . . . . 5 (∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥) → ¬ ∀𝑥 ¬ ∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥))
4 df-ex 1696 . . . . 5 (∃𝑥𝑦(∀𝑥⊥ → 𝑦 = 𝑥) ↔ ¬ ∀𝑥 ¬ ∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥))
53, 4sylibr 223 . . . 4 (∀𝑦(∀𝑥⊥ → 𝑦 = 𝑥) → ∃𝑥𝑦(∀𝑥⊥ → 𝑦 = 𝑥))
6 fal 1482 . . . . . 6 ¬ ⊥
7 sp 2041 . . . . . 6 (∀𝑥⊥ → ⊥)
86, 7mto 187 . . . . 5 ¬ ∀𝑥
98pm2.21i 115 . . . 4 (∀𝑥⊥ → 𝑦 = 𝑥)
105, 9mpg 1715 . . 3 𝑥𝑦(∀𝑥⊥ → 𝑦 = 𝑥)
111, 10mpg 1715 . 2 𝑥𝑦(𝑦𝑥 ↔ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥))
128intnan 951 . . . . . 6 ¬ (𝑤𝑧 ∧ ∀𝑥⊥)
1312nex 1722 . . . . 5 ¬ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥)
1413nbn 361 . . . 4 𝑦𝑥 ↔ (𝑦𝑥 ↔ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥)))
1514albii 1737 . . 3 (∀𝑦 ¬ 𝑦𝑥 ↔ ∀𝑦(𝑦𝑥 ↔ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥)))
1615exbii 1764 . 2 (∃𝑥𝑦 ¬ 𝑦𝑥 ↔ ∃𝑥𝑦(𝑦𝑥 ↔ ∃𝑤(𝑤𝑧 ∧ ∀𝑥⊥)))
1711, 16mpbir 220 1 𝑥𝑦 ¬ 𝑦𝑥
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wa 383  wal 1473   = wceq 1475  wfal 1480  wex 1695  wcel 1977
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-12 2034  ax-rep 4694
This theorem depends on definitions:  df-bi 196  df-an 385  df-tru 1478  df-fal 1481  df-ex 1696
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator