Theorem nnnn0 9505

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

Syntax hints:   -> wi 4   e. wcel 2205   NNcn 9239   NN0cn0 9498

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 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3217  df-in 3219  df-ss 3226  df-n0 9499

This theorem is referenced by:  nnnn0i  9506  elnnnn0b  9542  elnnnn0c  9543  elnn0z  9592  elz2  9651  nn0ind-raph  9698  zindd  9699  fzo1fzo0n0  10526  ubmelfzo  10549  elfzom1elp1fzo  10551  fzo0sn0fzo1  10570  modqmulnn  10708  expnegap0  10913  expcllem  10916  expcl2lemap  10917  expap0  10935  expeq0  10936  mulexpzap  10945  expnlbnd  11030  apexp1  11084  facdiv  11104  faclbnd  11107  faclbnd3  11109  faclbnd6  11110  pfxn0  11384  resqrexlemlo  11702  absexpzap  11769  nnf1o  12066  summodclem2a  12071  fsum3  12077  arisum  12188  expcnvap0  12192  expcnv  12194  geo2sum  12204  geo2lim  12206  geoisum1c  12210  0.999...  12211  mertenslem2  12226  fprodseq  12273  fprodfac  12305  ef0lem  12350  ege2le3  12361  efaddlem  12364  efexp  12372  dvdsmodexp  12485  nn0enne  12592  nnehalf  12594  nno  12596  nn0o  12597  divalg2  12616  ndvdssub  12620  gcddiv  12719  gcdmultiple  12720  gcdmultiplez  12721  rpmulgcd  12726  rplpwr  12727  dvdssqlem  12730  eucalgf  12756  1nprm  12815  isprm6  12848  prmdvdsexp  12849  pw2dvds  12867  oddpwdc  12875  phicl2  12915  phibndlem  12917  phiprmpw  12923  crth  12925  hashgcdlem  12939  phisum  12942  pythagtriplem10  12971  pythagtriplem6  12972  pythagtriplem7  12973  pythagtriplem12  12977  pythagtriplem14  12979  pclemub  12989  pcexp  13011  pcid  13026  pcprod  13048  pcbc  13053  prmpwdvds  13057  infpnlem1  13061  infpnlem2  13062  prmunb  13064  1arith  13069  ennnfonelemjn  13170  ghmmulg  13990  znf1o  14816  znfi  14820  znhash  14821  znidom  14822  znidomb  14823  znrrg  14825  dvexp  15593  plycolemc  15640  logbgcd1irr  15849  pellexlem1  15862  1sgm2ppw  15880  lgsval4a  15912  gausslemma2dlem0c  15941  gausslemma2dlem0d  15942  gausslemma2dlem6  15957  2lgslem1a1  15976  2lgslem1c  15980  2lgslem3a1  15987  2lgslem3b1  15988  2lgslem3c1  15989  2lgslem3d1  15990  isclwwlknx  16428