Theorem nnnn0 9409

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

Syntax hints:   -> wi 4   e. wcel 2202   NNcn 9143   NN0cn0 9402

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-n0 9403

This theorem is referenced by:  nnnn0i  9410  elnnnn0b  9446  elnnnn0c  9447  elnn0z  9492  elz2  9551  nn0ind-raph  9597  zindd  9598  fzo1fzo0n0  10423  ubmelfzo  10446  elfzom1elp1fzo  10448  fzo0sn0fzo1  10467  modqmulnn  10605  expnegap0  10810  expcllem  10813  expcl2lemap  10814  expap0  10832  expeq0  10833  mulexpzap  10842  expnlbnd  10927  apexp1  10981  facdiv  11001  faclbnd  11004  faclbnd3  11006  faclbnd6  11007  pfxn0  11273  resqrexlemlo  11591  absexpzap  11658  nnf1o  11955  summodclem2a  11960  fsum3  11966  arisum  12077  expcnvap0  12081  expcnv  12083  geo2sum  12093  geo2lim  12095  geoisum1c  12099  0.999...  12100  mertenslem2  12115  fprodseq  12162  fprodfac  12194  ef0lem  12239  ege2le3  12250  efaddlem  12253  efexp  12261  dvdsmodexp  12374  nn0enne  12481  nnehalf  12483  nno  12485  nn0o  12486  divalg2  12505  ndvdssub  12509  gcddiv  12608  gcdmultiple  12609  gcdmultiplez  12610  rpmulgcd  12615  rplpwr  12616  dvdssqlem  12619  eucalgf  12645  1nprm  12704  isprm6  12737  prmdvdsexp  12738  pw2dvds  12756  oddpwdc  12764  phicl2  12804  phibndlem  12806  phiprmpw  12812  crth  12814  hashgcdlem  12828  phisum  12831  pythagtriplem10  12860  pythagtriplem6  12861  pythagtriplem7  12862  pythagtriplem12  12866  pythagtriplem14  12868  pclemub  12878  pcexp  12900  pcid  12915  pcprod  12937  pcbc  12942  prmpwdvds  12946  infpnlem1  12950  infpnlem2  12951  prmunb  12953  1arith  12958  ennnfonelemjn  13041  ghmmulg  13861  znf1o  14684  znfi  14688  znhash  14689  znidom  14690  znidomb  14691  znrrg  14693  dvexp  15454  plycolemc  15501  logbgcd1irr  15710  1sgm2ppw  15738  lgsval4a  15770  gausslemma2dlem0c  15799  gausslemma2dlem0d  15800  gausslemma2dlem6  15815  2lgslem1a1  15834  2lgslem1c  15838  2lgslem3a1  15845  2lgslem3b1  15846  2lgslem3c1  15847  2lgslem3d1  15848  isclwwlknx  16286