Theorem nnnn0 9451

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

Syntax hints:   -> wi 4   e. wcel 2202   NNcn 9185   NN0cn0 9444

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 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-n0 9445

This theorem is referenced by:  nnnn0i  9452  elnnnn0b  9488  elnnnn0c  9489  elnn0z  9536  elz2  9595  nn0ind-raph  9641  zindd  9642  fzo1fzo0n0  10468  ubmelfzo  10491  elfzom1elp1fzo  10493  fzo0sn0fzo1  10512  modqmulnn  10650  expnegap0  10855  expcllem  10858  expcl2lemap  10859  expap0  10877  expeq0  10878  mulexpzap  10887  expnlbnd  10972  apexp1  11026  facdiv  11046  faclbnd  11049  faclbnd3  11051  faclbnd6  11052  pfxn0  11318  resqrexlemlo  11636  absexpzap  11703  nnf1o  12000  summodclem2a  12005  fsum3  12011  arisum  12122  expcnvap0  12126  expcnv  12128  geo2sum  12138  geo2lim  12140  geoisum1c  12144  0.999...  12145  mertenslem2  12160  fprodseq  12207  fprodfac  12239  ef0lem  12284  ege2le3  12295  efaddlem  12298  efexp  12306  dvdsmodexp  12419  nn0enne  12526  nnehalf  12528  nno  12530  nn0o  12531  divalg2  12550  ndvdssub  12554  gcddiv  12653  gcdmultiple  12654  gcdmultiplez  12655  rpmulgcd  12660  rplpwr  12661  dvdssqlem  12664  eucalgf  12690  1nprm  12749  isprm6  12782  prmdvdsexp  12783  pw2dvds  12801  oddpwdc  12809  phicl2  12849  phibndlem  12851  phiprmpw  12857  crth  12859  hashgcdlem  12873  phisum  12876  pythagtriplem10  12905  pythagtriplem6  12906  pythagtriplem7  12907  pythagtriplem12  12911  pythagtriplem14  12913  pclemub  12923  pcexp  12945  pcid  12960  pcprod  12982  pcbc  12987  prmpwdvds  12991  infpnlem1  12995  infpnlem2  12996  prmunb  12998  1arith  13003  ennnfonelemjn  13086  ghmmulg  13906  znf1o  14730  znfi  14734  znhash  14735  znidom  14736  znidomb  14737  znrrg  14739  dvexp  15505  plycolemc  15552  logbgcd1irr  15761  pellexlem1  15774  1sgm2ppw  15792  lgsval4a  15824  gausslemma2dlem0c  15853  gausslemma2dlem0d  15854  gausslemma2dlem6  15869  2lgslem1a1  15888  2lgslem1c  15892  2lgslem3a1  15899  2lgslem3b1  15900  2lgslem3c1  15901  2lgslem3d1  15902  isclwwlknx  16340