Theorem nnnn0 9574

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   NNcn 9306   NN0cn0 9567

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-n0 9568

This theorem is used by:  nnnn0i  9575  elnnnn0b  9611  elnnnn0c  9612  elnn0z  9661  elz2  9720  nn0ind-raph  9767  zindd  9768  fzo1fzo0n0  10605  ubmelfzo  10628  elfzom1elp1fzo  10630  fzo0sn0fzo1  10649  modqmulnn  10792  expnegap0  10997  expcllem  11000  expcl2lemap  11001  expap0  11019  expeq0  11020  mulexpzap  11029  expnlbnd  11115  apexp1  11170  facdiv  11190  faclbnd  11193  faclbnd3  11195  faclbnd6  11196  pfxn0  11474  resqrexlemlo  11793  absexpzap  11861  nnf1o  12159  summodclem2a  12164  fsum3  12170  arisum  12281  expcnvap0  12285  expcnv  12287  geo2sum  12297  geo2lim  12299  geoisum1c  12303  0.999...  12304  mertenslem2  12319  fprodseq  12366  fprodfac  12398  ef0lem  12443  ege2le3  12454  efaddlem  12457  efexp  12465  dvdsmodexp  12578  nn0enne  12685  nnehalf  12687  nno  12689  nn0o  12690  divalg2  12709  ndvdssub  12713  gcddiv  12812  gcdmultiple  12813  gcdmultiplez  12814  rpmulgcd  12819  rplpwr  12820  dvdssqlem  12823  eucalgf  12849  1nprm  12908  isprm6  12942  prmdvdsexp  12943  pwbdvdslemn  12960  phicl2  13012  phibndlem  13014  phiprmpw  13020  crth  13022  hashgcdlem  13036  phisum  13039  pythagtriplem10  13068  pythagtriplem6  13069  pythagtriplem7  13070  pythagtriplem12  13074  pythagtriplem14  13076  pclemub  13086  pcexp  13108  pcid  13123  pcprod  13145  pcbc  13150  prmpwdvds  13154  infpnlem1  13158  infpnlem2  13159  prmunb  13161  1arith  13166  ennnfonelemjn  13342  ghmmulg  14108  znf1o  15035  znfi  15039  znhash  15040  znidom  15041  znidomb  15042  znrrg  15044  dvexp  15861  plycolemc  15908  logbgcd1irr  16122  birthdaylem2  16145  birthdaylem3  16146  pellexlem1  16148  1sgm2ppw  16190  pcbcctr  16201  bclbnd  16205  bposlem1  16209  lgsval4a  16239  gausslemma2dlem0c  16268  gausslemma2dlem0d  16269  gausslemma2dlem6  16284  2lgslem1a1  16303  2lgslem1c  16307  2lgslem3a1  16314  2lgslem3b1  16315  2lgslem3c1  16316  2lgslem3d1  16317  isclwwlknx  16755