Theorem nnnn0 8613

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

Syntax hints:   -> wi 4   e. wcel 1436   NNcn 8357   NN0cn0 8606

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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-un 2992  df-in 2994  df-ss 3001  df-n0 8607

This theorem is referenced by:  nnnn0i  8614  elnnnn0b  8650  elnnnn0c  8651  elnn0z  8696  elz2  8751  nn0ind-raph  8796  zindd  8797  fzo1fzo0n0  9522  ubmelfzo  9539  elfzom1elp1fzo  9541  fzo0sn0fzo1  9560  modqmulnn  9677  expnegap0  9861  expcllem  9864  expcl2lemap  9865  expap0  9883  expeq0  9884  mulexpzap  9893  expnlbnd  9974  facdiv  10042  faclbnd  10045  faclbnd3  10047  faclbnd6  10048  resqrexlemlo  10341  absexpzap  10408  isummolemnm  10658  isummolem2a  10660  fisum  10665  nn0enne  10777  nnehalf  10779  nno  10781  nn0o  10782  divalg2  10801  ndvdssub  10805  gcddiv  10883  gcdmultiple  10884  gcdmultiplez  10885  rpmulgcd  10890  rplpwr  10891  dvdssqlem  10894  eucalgf  10912  1nprm  10971  isprm6  11001  prmdvdsexp  11002  pw2dvds  11019  oddpwdc  11027  phicl2  11065  phibndlem  11067  phiprmpw  11073  crth  11075  hashgcdlem  11078