Theorem nnnn0 9570

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   NNcn 9304   NN0cn0 9563

This proof depends on 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 proof 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 9564

This theorem is used by:  nnnn0i  9571  elnnnn0b  9607  elnnnn0c  9608  elnn0z  9657  elz2  9716  nn0ind-raph  9763  zindd  9764  fzo1fzo0n0  10595  ubmelfzo  10618  elfzom1elp1fzo  10620  fzo0sn0fzo1  10639  modqmulnn  10779  expnegap0  10984  expcllem  10987  expcl2lemap  10988  expap0  11006  expeq0  11007  mulexpzap  11016  expnlbnd  11102  apexp1  11156  facdiv  11176  faclbnd  11179  faclbnd3  11181  faclbnd6  11182  pfxn0  11460  resqrexlemlo  11779  absexpzap  11846  nnf1o  12143  summodclem2a  12148  fsum3  12154  arisum  12265  expcnvap0  12269  expcnv  12271  geo2sum  12281  geo2lim  12283  geoisum1c  12287  0.999...  12288  mertenslem2  12303  fprodseq  12350  fprodfac  12382  ef0lem  12427  ege2le3  12438  efaddlem  12441  efexp  12449  dvdsmodexp  12562  nn0enne  12669  nnehalf  12671  nno  12673  nn0o  12674  divalg2  12693  ndvdssub  12697  gcddiv  12796  gcdmultiple  12797  gcdmultiplez  12798  rpmulgcd  12803  rplpwr  12804  dvdssqlem  12807  eucalgf  12833  1nprm  12892  isprm6  12925  prmdvdsexp  12926  pw2dvds  12944  oddpwdc  12952  phicl2  12992  phibndlem  12994  phiprmpw  13000  crth  13002  hashgcdlem  13016  phisum  13019  pythagtriplem10  13048  pythagtriplem6  13049  pythagtriplem7  13050  pythagtriplem12  13054  pythagtriplem14  13056  pclemub  13066  pcexp  13088  pcid  13103  pcprod  13125  pcbc  13130  prmpwdvds  13134  infpnlem1  13138  infpnlem2  13139  prmunb  13141  1arith  13146  ennnfonelemjn  13293  ghmmulg  14059  znf1o  14986  znfi  14990  znhash  14991  znidom  14992  znidomb  14993  znrrg  14995  dvexp  15812  plycolemc  15859  logbgcd1irr  16069  birthdaylem2  16088  birthdaylem3  16089  pellexlem1  16091  1sgm2ppw  16109  lgsval4a  16141  gausslemma2dlem0c  16170  gausslemma2dlem0d  16171  gausslemma2dlem6  16186  2lgslem1a1  16205  2lgslem1c  16209  2lgslem3a1  16216  2lgslem3b1  16217  2lgslem3c1  16218  2lgslem3d1  16219  isclwwlknx  16657