Theorem nnnn0 9275

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

Syntax hints:   -> wi 4   e. wcel 2167   NNcn 9009   NN0cn0 9268

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 9269

This theorem is referenced by:  nnnn0i  9276  elnnnn0b  9312  elnnnn0c  9313  elnn0z  9358  elz2  9416  nn0ind-raph  9462  zindd  9463  fzo1fzo0n0  10278  ubmelfzo  10295  elfzom1elp1fzo  10297  fzo0sn0fzo1  10316  modqmulnn  10453  expnegap0  10658  expcllem  10661  expcl2lemap  10662  expap0  10680  expeq0  10681  mulexpzap  10690  expnlbnd  10775  apexp1  10829  facdiv  10849  faclbnd  10852  faclbnd3  10854  faclbnd6  10855  resqrexlemlo  11197  absexpzap  11264  nnf1o  11560  summodclem2a  11565  fsum3  11571  arisum  11682  expcnvap0  11686  expcnv  11688  geo2sum  11698  geo2lim  11700  geoisum1c  11704  0.999...  11705  mertenslem2  11720  fprodseq  11767  fprodfac  11799  ef0lem  11844  ege2le3  11855  efaddlem  11858  efexp  11866  dvdsmodexp  11979  nn0enne  12086  nnehalf  12088  nno  12090  nn0o  12091  divalg2  12110  ndvdssub  12114  gcddiv  12213  gcdmultiple  12214  gcdmultiplez  12215  rpmulgcd  12220  rplpwr  12221  dvdssqlem  12224  eucalgf  12250  1nprm  12309  isprm6  12342  prmdvdsexp  12343  pw2dvds  12361  oddpwdc  12369  phicl2  12409  phibndlem  12411  phiprmpw  12417  crth  12419  hashgcdlem  12433  phisum  12436  pythagtriplem10  12465  pythagtriplem6  12466  pythagtriplem7  12467  pythagtriplem12  12471  pythagtriplem14  12473  pclemub  12483  pcexp  12505  pcid  12520  pcprod  12542  pcbc  12547  prmpwdvds  12551  infpnlem1  12555  infpnlem2  12556  prmunb  12558  1arith  12563  ennnfonelemjn  12646  ghmmulg  13464  znf1o  14285  znfi  14289  znhash  14290  znidom  14291  znidomb  14292  znrrg  14294  dvexp  15055  plycolemc  15102  logbgcd1irr  15311  1sgm2ppw  15339  lgsval4a  15371  gausslemma2dlem0c  15400  gausslemma2dlem0d  15401  gausslemma2dlem6  15416  2lgslem1a1  15435  2lgslem1c  15439  2lgslem3a1  15446  2lgslem3b1  15447  2lgslem3c1  15448  2lgslem3d1  15449