Theorem nnnn0 9399

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

Syntax hints:   -> wi 4   e. wcel 2200   NNcn 9133   NN0cn0 9392

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-un 3202  df-in 3204  df-ss 3211  df-n0 9393

This theorem is referenced by:  nnnn0i  9400  elnnnn0b  9436  elnnnn0c  9437  elnn0z  9482  elz2  9541  nn0ind-raph  9587  zindd  9588  fzo1fzo0n0  10412  ubmelfzo  10435  elfzom1elp1fzo  10437  fzo0sn0fzo1  10456  modqmulnn  10594  expnegap0  10799  expcllem  10802  expcl2lemap  10803  expap0  10821  expeq0  10822  mulexpzap  10831  expnlbnd  10916  apexp1  10970  facdiv  10990  faclbnd  10993  faclbnd3  10995  faclbnd6  10996  pfxn0  11259  resqrexlemlo  11564  absexpzap  11631  nnf1o  11927  summodclem2a  11932  fsum3  11938  arisum  12049  expcnvap0  12053  expcnv  12055  geo2sum  12065  geo2lim  12067  geoisum1c  12071  0.999...  12072  mertenslem2  12087  fprodseq  12134  fprodfac  12166  ef0lem  12211  ege2le3  12222  efaddlem  12225  efexp  12233  dvdsmodexp  12346  nn0enne  12453  nnehalf  12455  nno  12457  nn0o  12458  divalg2  12477  ndvdssub  12481  gcddiv  12580  gcdmultiple  12581  gcdmultiplez  12582  rpmulgcd  12587  rplpwr  12588  dvdssqlem  12591  eucalgf  12617  1nprm  12676  isprm6  12709  prmdvdsexp  12710  pw2dvds  12728  oddpwdc  12736  phicl2  12776  phibndlem  12778  phiprmpw  12784  crth  12786  hashgcdlem  12800  phisum  12803  pythagtriplem10  12832  pythagtriplem6  12833  pythagtriplem7  12834  pythagtriplem12  12838  pythagtriplem14  12840  pclemub  12850  pcexp  12872  pcid  12887  pcprod  12909  pcbc  12914  prmpwdvds  12918  infpnlem1  12922  infpnlem2  12923  prmunb  12925  1arith  12930  ennnfonelemjn  13013  ghmmulg  13833  znf1o  14655  znfi  14659  znhash  14660  znidom  14661  znidomb  14662  znrrg  14664  dvexp  15425  plycolemc  15472  logbgcd1irr  15681  1sgm2ppw  15709  lgsval4a  15741  gausslemma2dlem0c  15770  gausslemma2dlem0d  15771  gausslemma2dlem6  15786  2lgslem1a1  15805  2lgslem1c  15809  2lgslem3a1  15816  2lgslem3b1  15817  2lgslem3c1  15818  2lgslem3d1  15819  isclwwlknx  16211