Theorem nnnn0 9549

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

Syntax hints:   -> wi 4   e. wcel 2209   NNcn 9283   NN0cn0 9542

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-n0 9543

This theorem is referenced by:  nnnn0i  9550  elnnnn0b  9586  elnnnn0c  9587  elnn0z  9636  elz2  9695  nn0ind-raph  9742  zindd  9743  fzo1fzo0n0  10573  ubmelfzo  10596  elfzom1elp1fzo  10598  fzo0sn0fzo1  10617  modqmulnn  10757  expnegap0  10962  expcllem  10965  expcl2lemap  10966  expap0  10984  expeq0  10985  mulexpzap  10994  expnlbnd  11080  apexp1  11134  facdiv  11154  faclbnd  11157  faclbnd3  11159  faclbnd6  11160  pfxn0  11438  resqrexlemlo  11757  absexpzap  11824  nnf1o  12121  summodclem2a  12126  fsum3  12132  arisum  12243  expcnvap0  12247  expcnv  12249  geo2sum  12259  geo2lim  12261  geoisum1c  12265  0.999...  12266  mertenslem2  12281  fprodseq  12328  fprodfac  12360  ef0lem  12405  ege2le3  12416  efaddlem  12419  efexp  12427  dvdsmodexp  12540  nn0enne  12647  nnehalf  12649  nno  12651  nn0o  12652  divalg2  12671  ndvdssub  12675  gcddiv  12774  gcdmultiple  12775  gcdmultiplez  12776  rpmulgcd  12781  rplpwr  12782  dvdssqlem  12785  eucalgf  12811  1nprm  12870  isprm6  12903  prmdvdsexp  12904  pw2dvds  12922  oddpwdc  12930  phicl2  12970  phibndlem  12972  phiprmpw  12978  crth  12980  hashgcdlem  12994  phisum  12997  pythagtriplem10  13026  pythagtriplem6  13027  pythagtriplem7  13028  pythagtriplem12  13032  pythagtriplem14  13034  pclemub  13044  pcexp  13066  pcid  13081  pcprod  13103  pcbc  13108  prmpwdvds  13112  infpnlem1  13116  infpnlem2  13117  prmunb  13119  1arith  13124  ennnfonelemjn  13271  ghmmulg  14036  znf1o  14958  znfi  14962  znhash  14963  znidom  14964  znidomb  14965  znrrg  14967  dvexp  15735  plycolemc  15782  logbgcd1irr  15992  pellexlem1  16005  1sgm2ppw  16023  lgsval4a  16055  gausslemma2dlem0c  16084  gausslemma2dlem0d  16085  gausslemma2dlem6  16100  2lgslem1a1  16119  2lgslem1c  16123  2lgslem3a1  16130  2lgslem3b1  16131  2lgslem3c1  16132  2lgslem3d1  16133  isclwwlknx  16571