Theorem nnnn0 8432

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

Syntax hints:   -> wi 4   e. wcel 1434   NNcn 8176   NN0cn0 8425

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-v 2612  df-un 2986  df-in 2988  df-ss 2995  df-n0 8426

This theorem is referenced by:  nnnn0i  8433  elnnnn0b  8469  elnnnn0c  8470  elnn0z  8515  elz2  8570  nn0ind-raph  8615  zindd  8616  fzo1fzo0n0  9339  ubmelfzo  9356  elfzom1elp1fzo  9358  fzo0sn0fzo1  9377  modqmulnn  9494  expnegap0  9651  expcllem  9654  expcl2lemap  9655  expap0  9673  expeq0  9674  mulexpzap  9683  expnlbnd  9764  facdiv  9832  faclbnd  9835  faclbnd3  9837  faclbnd6  9838  resqrexlemlo  10118  absexpzap  10185  nn0enne  10527  nnehalf  10529  nno  10531  nn0o  10532  divalg2  10551  ndvdssub  10555  gcddiv  10633  gcdmultiple  10634  gcdmultiplez  10635  rpmulgcd  10640  rplpwr  10641  dvdssqlem  10644  eucalgf  10662  1nprm  10721  isprm6  10751  prmdvdsexp  10752  pw2dvds  10769  oddpwdc  10777  phicl2  10815  phibndlem  10817  phiprmpw  10823  crth  10825  hashgcdlem  10828