Theorem nnnn0 9185

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

Syntax hints:   -> wi 4   e. wcel 2148   NNcn 8921   NN0cn0 9178

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2741  df-un 3135  df-in 3137  df-ss 3144  df-n0 9179

This theorem is referenced by:  nnnn0i  9186  elnnnn0b  9222  elnnnn0c  9223  elnn0z  9268  elz2  9326  nn0ind-raph  9372  zindd  9373  fzo1fzo0n0  10185  ubmelfzo  10202  elfzom1elp1fzo  10204  fzo0sn0fzo1  10223  modqmulnn  10344  expnegap0  10530  expcllem  10533  expcl2lemap  10534  expap0  10552  expeq0  10553  mulexpzap  10562  expnlbnd  10647  apexp1  10700  facdiv  10720  faclbnd  10723  faclbnd3  10725  faclbnd6  10726  resqrexlemlo  11024  absexpzap  11091  nnf1o  11386  summodclem2a  11391  fsum3  11397  arisum  11508  expcnvap0  11512  expcnv  11514  geo2sum  11524  geo2lim  11526  geoisum1c  11530  0.999...  11531  mertenslem2  11546  fprodseq  11593  fprodfac  11625  ef0lem  11670  ege2le3  11681  efaddlem  11684  efexp  11692  dvdsmodexp  11804  nn0enne  11909  nnehalf  11911  nno  11913  nn0o  11914  divalg2  11933  ndvdssub  11937  gcddiv  12022  gcdmultiple  12023  gcdmultiplez  12024  rpmulgcd  12029  rplpwr  12030  dvdssqlem  12033  eucalgf  12057  1nprm  12116  isprm6  12149  prmdvdsexp  12150  pw2dvds  12168  oddpwdc  12176  phicl2  12216  phibndlem  12218  phiprmpw  12224  crth  12226  hashgcdlem  12240  phisum  12242  pythagtriplem10  12271  pythagtriplem6  12272  pythagtriplem7  12273  pythagtriplem12  12277  pythagtriplem14  12279  pclemub  12289  pcexp  12311  pcid  12325  pcprod  12346  pcbc  12351  prmpwdvds  12355  infpnlem1  12359  infpnlem2  12360  prmunb  12362  1arith  12367  ennnfonelemjn  12405  dvexp  14214  logbgcd1irr  14424  lgsval4a  14462