Theorem nnnn0 9372

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

Syntax hints:   -> wi 4   e. wcel 2200   NNcn 9106   NN0cn0 9365

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 2801  df-un 3201  df-in 3203  df-ss 3210  df-n0 9366

This theorem is referenced by:  nnnn0i  9373  elnnnn0b  9409  elnnnn0c  9410  elnn0z  9455  elz2  9514  nn0ind-raph  9560  zindd  9561  fzo1fzo0n0  10379  ubmelfzo  10401  elfzom1elp1fzo  10403  fzo0sn0fzo1  10422  modqmulnn  10559  expnegap0  10764  expcllem  10767  expcl2lemap  10768  expap0  10786  expeq0  10787  mulexpzap  10796  expnlbnd  10881  apexp1  10935  facdiv  10955  faclbnd  10958  faclbnd3  10960  faclbnd6  10961  pfxn0  11215  resqrexlemlo  11519  absexpzap  11586  nnf1o  11882  summodclem2a  11887  fsum3  11893  arisum  12004  expcnvap0  12008  expcnv  12010  geo2sum  12020  geo2lim  12022  geoisum1c  12026  0.999...  12027  mertenslem2  12042  fprodseq  12089  fprodfac  12121  ef0lem  12166  ege2le3  12177  efaddlem  12180  efexp  12188  dvdsmodexp  12301  nn0enne  12408  nnehalf  12410  nno  12412  nn0o  12413  divalg2  12432  ndvdssub  12436  gcddiv  12535  gcdmultiple  12536  gcdmultiplez  12537  rpmulgcd  12542  rplpwr  12543  dvdssqlem  12546  eucalgf  12572  1nprm  12631  isprm6  12664  prmdvdsexp  12665  pw2dvds  12683  oddpwdc  12691  phicl2  12731  phibndlem  12733  phiprmpw  12739  crth  12741  hashgcdlem  12755  phisum  12758  pythagtriplem10  12787  pythagtriplem6  12788  pythagtriplem7  12789  pythagtriplem12  12793  pythagtriplem14  12795  pclemub  12805  pcexp  12827  pcid  12842  pcprod  12864  pcbc  12869  prmpwdvds  12873  infpnlem1  12877  infpnlem2  12878  prmunb  12880  1arith  12885  ennnfonelemjn  12968  ghmmulg  13788  znf1o  14609  znfi  14613  znhash  14614  znidom  14615  znidomb  14616  znrrg  14618  dvexp  15379  plycolemc  15426  logbgcd1irr  15635  1sgm2ppw  15663  lgsval4a  15695  gausslemma2dlem0c  15724  gausslemma2dlem0d  15725  gausslemma2dlem6  15740  2lgslem1a1  15759  2lgslem1c  15763  2lgslem3a1  15770  2lgslem3b1  15771  2lgslem3c1  15772  2lgslem3d1  15773