Theorem nnnn0 9259

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

Syntax hints:   -> wi 4   e. wcel 2167   NNcn 8993   NN0cn0 9252

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-n0 9253

This theorem is referenced by:  nnnn0i  9260  elnnnn0b  9296  elnnnn0c  9297  elnn0z  9342  elz2  9400  nn0ind-raph  9446  zindd  9447  fzo1fzo0n0  10262  ubmelfzo  10279  elfzom1elp1fzo  10281  fzo0sn0fzo1  10300  modqmulnn  10437  expnegap0  10642  expcllem  10645  expcl2lemap  10646  expap0  10664  expeq0  10665  mulexpzap  10674  expnlbnd  10759  apexp1  10813  facdiv  10833  faclbnd  10836  faclbnd3  10838  faclbnd6  10839  resqrexlemlo  11181  absexpzap  11248  nnf1o  11544  summodclem2a  11549  fsum3  11555  arisum  11666  expcnvap0  11670  expcnv  11672  geo2sum  11682  geo2lim  11684  geoisum1c  11688  0.999...  11689  mertenslem2  11704  fprodseq  11751  fprodfac  11783  ef0lem  11828  ege2le3  11839  efaddlem  11842  efexp  11850  dvdsmodexp  11963  nn0enne  12070  nnehalf  12072  nno  12074  nn0o  12075  divalg2  12094  ndvdssub  12098  gcddiv  12197  gcdmultiple  12198  gcdmultiplez  12199  rpmulgcd  12204  rplpwr  12205  dvdssqlem  12208  eucalgf  12234  1nprm  12293  isprm6  12326  prmdvdsexp  12327  pw2dvds  12345  oddpwdc  12353  phicl2  12393  phibndlem  12395  phiprmpw  12401  crth  12403  hashgcdlem  12417  phisum  12420  pythagtriplem10  12449  pythagtriplem6  12450  pythagtriplem7  12451  pythagtriplem12  12455  pythagtriplem14  12457  pclemub  12467  pcexp  12489  pcid  12504  pcprod  12526  pcbc  12531  prmpwdvds  12535  infpnlem1  12539  infpnlem2  12540  prmunb  12542  1arith  12547  ennnfonelemjn  12630  ghmmulg  13412  znf1o  14233  znfi  14237  znhash  14238  znidom  14239  znidomb  14240  znrrg  14242  dvexp  14973  plycolemc  15020  logbgcd1irr  15229  1sgm2ppw  15257  lgsval4a  15289  gausslemma2dlem0c  15318  gausslemma2dlem0d  15319  gausslemma2dlem6  15334  2lgslem1a1  15353  2lgslem1c  15357  2lgslem3a1  15364  2lgslem3b1  15365  2lgslem3c1  15366  2lgslem3d1  15367