Theorem nnnn0 9212

Description: A positive integer is a nonnegative integer. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nnnn0	|- ( A e. NN -> A e. NN0 )

Proof of Theorem nnnn0

Step	Hyp	Ref	Expression
1		nnssnn0 9208	. 2 |- NN C_ NN0
2	1	sseli 3166	1 |- ( A e. NN -> A e. NN0 )

Syntax hints:   -> wi 4   e. wcel 2160   NNcn 8948   NN0cn0 9205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-un 3148  df-in 3150  df-ss 3157  df-n0 9206

This theorem is referenced by:  nnnn0i  9213  elnnnn0b  9249  elnnnn0c  9250  elnn0z  9295  elz2  9353  nn0ind-raph  9399  zindd  9400  fzo1fzo0n0  10212  ubmelfzo  10229  elfzom1elp1fzo  10231  fzo0sn0fzo1  10250  modqmulnn  10372  expnegap0  10558  expcllem  10561  expcl2lemap  10562  expap0  10580  expeq0  10581  mulexpzap  10590  expnlbnd  10675  apexp1  10729  facdiv  10749  faclbnd  10752  faclbnd3  10754  faclbnd6  10755  resqrexlemlo  11053  absexpzap  11120  nnf1o  11415  summodclem2a  11420  fsum3  11426  arisum  11537  expcnvap0  11541  expcnv  11543  geo2sum  11553  geo2lim  11555  geoisum1c  11559  0.999...  11560  mertenslem2  11575  fprodseq  11622  fprodfac  11654  ef0lem  11699  ege2le3  11710  efaddlem  11713  efexp  11721  dvdsmodexp  11833  nn0enne  11938  nnehalf  11940  nno  11942  nn0o  11943  divalg2  11962  ndvdssub  11966  gcddiv  12051  gcdmultiple  12052  gcdmultiplez  12053  rpmulgcd  12058  rplpwr  12059  dvdssqlem  12062  eucalgf  12086  1nprm  12145  isprm6  12178  prmdvdsexp  12179  pw2dvds  12197  oddpwdc  12205  phicl2  12245  phibndlem  12247  phiprmpw  12253  crth  12255  hashgcdlem  12269  phisum  12271  pythagtriplem10  12300  pythagtriplem6  12301  pythagtriplem7  12302  pythagtriplem12  12306  pythagtriplem14  12308  pclemub  12318  pcexp  12340  pcid  12355  pcprod  12377  pcbc  12382  prmpwdvds  12386  infpnlem1  12390  infpnlem2  12391  prmunb  12393  1arith  12398  ennnfonelemjn  12452  ghmmulg  13192  dvexp  14627  logbgcd1irr  14837  lgsval4a  14876