Theorem nnnn0 9387

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

Syntax hints:   -> wi 4   e. wcel 2200   NNcn 9121   NN0cn0 9380

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-n0 9381

This theorem is referenced by:  nnnn0i  9388  elnnnn0b  9424  elnnnn0c  9425  elnn0z  9470  elz2  9529  nn0ind-raph  9575  zindd  9576  fzo1fzo0n0  10395  ubmelfzo  10418  elfzom1elp1fzo  10420  fzo0sn0fzo1  10439  modqmulnn  10576  expnegap0  10781  expcllem  10784  expcl2lemap  10785  expap0  10803  expeq0  10804  mulexpzap  10813  expnlbnd  10898  apexp1  10952  facdiv  10972  faclbnd  10975  faclbnd3  10977  faclbnd6  10978  pfxn0  11235  resqrexlemlo  11539  absexpzap  11606  nnf1o  11902  summodclem2a  11907  fsum3  11913  arisum  12024  expcnvap0  12028  expcnv  12030  geo2sum  12040  geo2lim  12042  geoisum1c  12046  0.999...  12047  mertenslem2  12062  fprodseq  12109  fprodfac  12141  ef0lem  12186  ege2le3  12197  efaddlem  12200  efexp  12208  dvdsmodexp  12321  nn0enne  12428  nnehalf  12430  nno  12432  nn0o  12433  divalg2  12452  ndvdssub  12456  gcddiv  12555  gcdmultiple  12556  gcdmultiplez  12557  rpmulgcd  12562  rplpwr  12563  dvdssqlem  12566  eucalgf  12592  1nprm  12651  isprm6  12684  prmdvdsexp  12685  pw2dvds  12703  oddpwdc  12711  phicl2  12751  phibndlem  12753  phiprmpw  12759  crth  12761  hashgcdlem  12775  phisum  12778  pythagtriplem10  12807  pythagtriplem6  12808  pythagtriplem7  12809  pythagtriplem12  12813  pythagtriplem14  12815  pclemub  12825  pcexp  12847  pcid  12862  pcprod  12884  pcbc  12889  prmpwdvds  12893  infpnlem1  12897  infpnlem2  12898  prmunb  12900  1arith  12905  ennnfonelemjn  12988  ghmmulg  13808  znf1o  14630  znfi  14634  znhash  14635  znidom  14636  znidomb  14637  znrrg  14639  dvexp  15400  plycolemc  15447  logbgcd1irr  15656  1sgm2ppw  15684  lgsval4a  15716  gausslemma2dlem0c  15745  gausslemma2dlem0d  15746  gausslemma2dlem6  15761  2lgslem1a1  15780  2lgslem1c  15784  2lgslem3a1  15791  2lgslem3b1  15792  2lgslem3c1  15793  2lgslem3d1  15794