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

Theorem nnnn0i 9973
Description: A natural number is a nonnegative integer. (Contributed by NM, 20-Jun-2005.)
Hypothesis
Ref Expression
nnnn0.1  |-  N  e.  NN
Assertion
Ref Expression
nnnn0i  |-  N  e. 
NN0

Proof of Theorem nnnn0i
StepHypRef Expression
1 nnnn0.1 . 2  |-  N  e.  NN
2 nnnn0 9972 . 2  |-  ( N  e.  NN  ->  N  e.  NN0 )
31, 2ax-mp 8 1  |-  N  e. 
NN0
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   NNcn 9746   NN0cn0 9965
This theorem is referenced by:  1nn0  9981  2nn0  9982  3nn0  9983  4nn0  9984  5nn0  9985  6nn0  9986  7nn0  9987  8nn0  9988  9nn0  9989  10nn0  9990  numlt  10143  numlti  10148  faclbnd4lem1  11306  divalglem6  12597  pockthi  12954  dec5dvds2  13080  modxp1i  13085  mod2xnegi  13086  43prm  13123  83prm  13124  317prm  13127  strlemor2  13236  strlemor3  13237  log2ublem2  20243  ballotlemfmpn  23053  ballotth  23096
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-in 3159  df-ss 3166  df-n0 9966
  Copyright terms: Public domain W3C validator