Theorem nnnn0 9503

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

Syntax hints:   -> wi 4   e. wcel 2203   NNcn 9237   NN0cn0 9496

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-un 3215  df-in 3217  df-ss 3224  df-n0 9497

This theorem is referenced by:  nnnn0i  9504  elnnnn0b  9540  elnnnn0c  9541  elnn0z  9590  elz2  9649  nn0ind-raph  9695  zindd  9696  fzo1fzo0n0  10522  ubmelfzo  10545  elfzom1elp1fzo  10547  fzo0sn0fzo1  10566  modqmulnn  10704  expnegap0  10909  expcllem  10912  expcl2lemap  10913  expap0  10931  expeq0  10932  mulexpzap  10941  expnlbnd  11026  apexp1  11080  facdiv  11100  faclbnd  11103  faclbnd3  11105  faclbnd6  11106  pfxn0  11380  resqrexlemlo  11698  absexpzap  11765  nnf1o  12062  summodclem2a  12067  fsum3  12073  arisum  12184  expcnvap0  12188  expcnv  12190  geo2sum  12200  geo2lim  12202  geoisum1c  12206  0.999...  12207  mertenslem2  12222  fprodseq  12269  fprodfac  12301  ef0lem  12346  ege2le3  12357  efaddlem  12360  efexp  12368  dvdsmodexp  12481  nn0enne  12588  nnehalf  12590  nno  12592  nn0o  12593  divalg2  12612  ndvdssub  12616  gcddiv  12715  gcdmultiple  12716  gcdmultiplez  12717  rpmulgcd  12722  rplpwr  12723  dvdssqlem  12726  eucalgf  12752  1nprm  12811  isprm6  12844  prmdvdsexp  12845  pw2dvds  12863  oddpwdc  12871  phicl2  12911  phibndlem  12913  phiprmpw  12919  crth  12921  hashgcdlem  12935  phisum  12938  pythagtriplem10  12967  pythagtriplem6  12968  pythagtriplem7  12969  pythagtriplem12  12973  pythagtriplem14  12975  pclemub  12985  pcexp  13007  pcid  13022  pcprod  13044  pcbc  13049  prmpwdvds  13053  infpnlem1  13057  infpnlem2  13058  prmunb  13060  1arith  13065  ennnfonelemjn  13153  ghmmulg  13973  znf1o  14799  znfi  14803  znhash  14804  znidom  14805  znidomb  14806  znrrg  14808  dvexp  15576  plycolemc  15623  logbgcd1irr  15832  pellexlem1  15845  1sgm2ppw  15863  lgsval4a  15895  gausslemma2dlem0c  15924  gausslemma2dlem0d  15925  gausslemma2dlem6  15940  2lgslem1a1  15959  2lgslem1c  15963  2lgslem3a1  15970  2lgslem3b1  15971  2lgslem3c1  15972  2lgslem3d1  15973  isclwwlknx  16411