Theorem nnnn0 9337

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

Syntax hints:   -> wi 4   e. wcel 2178   NNcn 9071   NN0cn0 9330

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-un 3178  df-in 3180  df-ss 3187  df-n0 9331

This theorem is referenced by:  nnnn0i  9338  elnnnn0b  9374  elnnnn0c  9375  elnn0z  9420  elz2  9479  nn0ind-raph  9525  zindd  9526  fzo1fzo0n0  10344  ubmelfzo  10366  elfzom1elp1fzo  10368  fzo0sn0fzo1  10387  modqmulnn  10524  expnegap0  10729  expcllem  10732  expcl2lemap  10733  expap0  10751  expeq0  10752  mulexpzap  10761  expnlbnd  10846  apexp1  10900  facdiv  10920  faclbnd  10923  faclbnd3  10925  faclbnd6  10926  pfxn0  11179  resqrexlemlo  11439  absexpzap  11506  nnf1o  11802  summodclem2a  11807  fsum3  11813  arisum  11924  expcnvap0  11928  expcnv  11930  geo2sum  11940  geo2lim  11942  geoisum1c  11946  0.999...  11947  mertenslem2  11962  fprodseq  12009  fprodfac  12041  ef0lem  12086  ege2le3  12097  efaddlem  12100  efexp  12108  dvdsmodexp  12221  nn0enne  12328  nnehalf  12330  nno  12332  nn0o  12333  divalg2  12352  ndvdssub  12356  gcddiv  12455  gcdmultiple  12456  gcdmultiplez  12457  rpmulgcd  12462  rplpwr  12463  dvdssqlem  12466  eucalgf  12492  1nprm  12551  isprm6  12584  prmdvdsexp  12585  pw2dvds  12603  oddpwdc  12611  phicl2  12651  phibndlem  12653  phiprmpw  12659  crth  12661  hashgcdlem  12675  phisum  12678  pythagtriplem10  12707  pythagtriplem6  12708  pythagtriplem7  12709  pythagtriplem12  12713  pythagtriplem14  12715  pclemub  12725  pcexp  12747  pcid  12762  pcprod  12784  pcbc  12789  prmpwdvds  12793  infpnlem1  12797  infpnlem2  12798  prmunb  12800  1arith  12805  ennnfonelemjn  12888  ghmmulg  13707  znf1o  14528  znfi  14532  znhash  14533  znidom  14534  znidomb  14535  znrrg  14537  dvexp  15298  plycolemc  15345  logbgcd1irr  15554  1sgm2ppw  15582  lgsval4a  15614  gausslemma2dlem0c  15643  gausslemma2dlem0d  15644  gausslemma2dlem6  15659  2lgslem1a1  15678  2lgslem1c  15682  2lgslem3a1  15689  2lgslem3b1  15690  2lgslem3c1  15691  2lgslem3d1  15692