Theorem nnnn0 9408

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

Syntax hints:   -> wi 4   e. wcel 2202   NNcn 9142   NN0cn0 9401

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 9402

This theorem is referenced by:  nnnn0i  9409  elnnnn0b  9445  elnnnn0c  9446  elnn0z  9491  elz2  9550  nn0ind-raph  9596  zindd  9597  fzo1fzo0n0  10421  ubmelfzo  10444  elfzom1elp1fzo  10446  fzo0sn0fzo1  10465  modqmulnn  10603  expnegap0  10808  expcllem  10811  expcl2lemap  10812  expap0  10830  expeq0  10831  mulexpzap  10840  expnlbnd  10925  apexp1  10979  facdiv  10999  faclbnd  11002  faclbnd3  11004  faclbnd6  11005  pfxn0  11268  resqrexlemlo  11573  absexpzap  11640  nnf1o  11936  summodclem2a  11941  fsum3  11947  arisum  12058  expcnvap0  12062  expcnv  12064  geo2sum  12074  geo2lim  12076  geoisum1c  12080  0.999...  12081  mertenslem2  12096  fprodseq  12143  fprodfac  12175  ef0lem  12220  ege2le3  12231  efaddlem  12234  efexp  12242  dvdsmodexp  12355  nn0enne  12462  nnehalf  12464  nno  12466  nn0o  12467  divalg2  12486  ndvdssub  12490  gcddiv  12589  gcdmultiple  12590  gcdmultiplez  12591  rpmulgcd  12596  rplpwr  12597  dvdssqlem  12600  eucalgf  12626  1nprm  12685  isprm6  12718  prmdvdsexp  12719  pw2dvds  12737  oddpwdc  12745  phicl2  12785  phibndlem  12787  phiprmpw  12793  crth  12795  hashgcdlem  12809  phisum  12812  pythagtriplem10  12841  pythagtriplem6  12842  pythagtriplem7  12843  pythagtriplem12  12847  pythagtriplem14  12849  pclemub  12859  pcexp  12881  pcid  12896  pcprod  12918  pcbc  12923  prmpwdvds  12927  infpnlem1  12931  infpnlem2  12932  prmunb  12934  1arith  12939  ennnfonelemjn  13022  ghmmulg  13842  znf1o  14664  znfi  14668  znhash  14669  znidom  14670  znidomb  14671  znrrg  14673  dvexp  15434  plycolemc  15481  logbgcd1irr  15690  1sgm2ppw  15718  lgsval4a  15750  gausslemma2dlem0c  15779  gausslemma2dlem0d  15780  gausslemma2dlem6  15795  2lgslem1a1  15814  2lgslem1c  15818  2lgslem3a1  15825  2lgslem3b1  15826  2lgslem3c1  15827  2lgslem3d1  15828  isclwwlknx  16266