Theorem nnnn0 9302

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 9298	. 2 |- NN C_ NN0
2	1	sseli 3189	1 |- ( A e. NN -> A e. NN0 )

Syntax hints:   -> wi 4   e. wcel 2176   NNcn 9036   NN0cn0 9295

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-n0 9296

This theorem is referenced by:  nnnn0i  9303  elnnnn0b  9339  elnnnn0c  9340  elnn0z  9385  elz2  9444  nn0ind-raph  9490  zindd  9491  fzo1fzo0n0  10307  ubmelfzo  10329  elfzom1elp1fzo  10331  fzo0sn0fzo1  10350  modqmulnn  10487  expnegap0  10692  expcllem  10695  expcl2lemap  10696  expap0  10714  expeq0  10715  mulexpzap  10724  expnlbnd  10809  apexp1  10863  facdiv  10883  faclbnd  10886  faclbnd3  10888  faclbnd6  10889  resqrexlemlo  11324  absexpzap  11391  nnf1o  11687  summodclem2a  11692  fsum3  11698  arisum  11809  expcnvap0  11813  expcnv  11815  geo2sum  11825  geo2lim  11827  geoisum1c  11831  0.999...  11832  mertenslem2  11847  fprodseq  11894  fprodfac  11926  ef0lem  11971  ege2le3  11982  efaddlem  11985  efexp  11993  dvdsmodexp  12106  nn0enne  12213  nnehalf  12215  nno  12217  nn0o  12218  divalg2  12237  ndvdssub  12241  gcddiv  12340  gcdmultiple  12341  gcdmultiplez  12342  rpmulgcd  12347  rplpwr  12348  dvdssqlem  12351  eucalgf  12377  1nprm  12436  isprm6  12469  prmdvdsexp  12470  pw2dvds  12488  oddpwdc  12496  phicl2  12536  phibndlem  12538  phiprmpw  12544  crth  12546  hashgcdlem  12560  phisum  12563  pythagtriplem10  12592  pythagtriplem6  12593  pythagtriplem7  12594  pythagtriplem12  12598  pythagtriplem14  12600  pclemub  12610  pcexp  12632  pcid  12647  pcprod  12669  pcbc  12674  prmpwdvds  12678  infpnlem1  12682  infpnlem2  12683  prmunb  12685  1arith  12690  ennnfonelemjn  12773  ghmmulg  13592  znf1o  14413  znfi  14417  znhash  14418  znidom  14419  znidomb  14420  znrrg  14422  dvexp  15183  plycolemc  15230  logbgcd1irr  15439  1sgm2ppw  15467  lgsval4a  15499  gausslemma2dlem0c  15528  gausslemma2dlem0d  15529  gausslemma2dlem6  15544  2lgslem1a1  15563  2lgslem1c  15567  2lgslem3a1  15574  2lgslem3b1  15575  2lgslem3c1  15576  2lgslem3d1  15577