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

Theorem axnulALT 4524
 Description: Alternate proof of axnul 4525, proved directly from ax-rep 4508 using none of the equality axioms ax-7 1859 through ax-c14 32527 provided we accept sp 1957 as an axiom. Replace sp 1957 with the obsolete ax-c5 32519 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 4508 . . 3
2 sp 1957 . . . . . 6
32con2i 124 . . . . 5
4 df-ex 1672 . . . . 5
53, 4sylibr 217 . . . 4
6 fal 1459 . . . . . 6
7 sp 1957 . . . . . 6
86, 7mto 181 . . . . 5
98pm2.21i 136 . . . 4
105, 9mpg 1679 . . 3
111, 10mpg 1679 . 2
128intnan 928 . . . . . 6
1312nex 1686 . . . . 5
1413nbn 354 . . . 4
1514albii 1699 . . 3
1615exbii 1726 . 2
1711, 16mpbir 214 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 189   wa 376  wal 1450   wceq 1452   wfal 1457  wex 1671   wcel 1904 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-12 1950  ax-rep 4508 This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-fal 1458  df-ex 1672 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator