MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nn0ex Structured version   Unicode version

Theorem nn0ex 10808
Description: The set of nonnegative integers exists. (Contributed by NM, 18-Jul-2004.)
Assertion
Ref Expression
nn0ex  |-  NN0  e.  _V

Proof of Theorem nn0ex
StepHypRef Expression
1 df-n0 10803 . 2  |-  NN0  =  ( NN  u.  { 0 } )
2 nnex 10549 . . 3  |-  NN  e.  _V
3 snex 4678 . . 3  |-  { 0 }  e.  _V
42, 3unex 6583 . 2  |-  ( NN  u.  { 0 } )  e.  _V
51, 4eqeltri 2527 1  |-  NN0  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1804   _Vcvv 3095    u. cun 3459   {csn 4014   0cc0 9495   NNcn 10543   NN0cn0 10802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-cnex 9551  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-i2m1 9563  ax-1ne0 9564  ax-rrecex 9567  ax-cnre 9568
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-ov 6284  df-om 6686  df-recs 7044  df-rdg 7078  df-nn 10544  df-n0 10803
This theorem is referenced by:  nn0ennn  12071  nnenom  12072  fsuppmapnn0fiub0  12081  suppssfz  12082  fsuppmapnn0ub  12083  mptnn0fsupp  12085  mptnn0fsuppr  12087  elovmptnn0wrd  12566  expcnv  13657  geolim  13661  cvgrat  13674  mertenslem2  13676  eftlub  13826  bitsfval  14055  bitsf  14059  sadfval  14084  smufval  14109  smupf  14110  1arith  14427  ramcl  14529  fsfnn0gsumfsffz  16990  gsummptnn0fz  16993  psrbag  17992  coe1fval  18223  fvcoe1  18225  coe1fval3  18226  coe1f2  18227  coe1sfi  18231  coe1sfiOLD  18232  coe1fsupp  18233  00ply1bas  18260  ply1plusgfvi  18262  coe1z  18283  coe1add  18284  coe1addfv  18285  coe1mul2lem1  18287  coe1mul2lem2  18288  coe1mul2  18289  coe1tm  18293  coe1sclmul  18302  coe1sclmulfv  18303  coe1sclmul2  18304  ply1coefsupp  18315  ply1coe  18316  ply1coeOLD  18317  gsumsmonply1  18324  gsummoncoe1  18325  evls1gsumadd  18340  evls1gsummul  18341  evl1gsummul  18375  nn0srg  18465  pmatcollpw1  19255  pmatcollpw2lem  19256  pmatcollpw2  19257  pmatcollpw3lem  19262  pm2mpcl  19276  idpm2idmp  19280  mply1topmatcllem  19282  mply1topmatcl  19284  mp2pm2mplem2  19286  mp2pm2mplem5  19289  mp2pm2mp  19290  pm2mpghmlem2  19291  pm2mpghm  19295  pm2mpmhmlem2  19298  monmat2matmon  19303  pm2mp  19304  chfacfscmulgsum  19339  chfacfpmmulgsum  19343  cpmidpmatlem2  19350  cpmadumatpolylem1  19360  cpmadumatpolylem2  19361  chcoeffeqlem  19364  cayhamlem3  19366  cayhamlem4  19367  dyadmax  21985  cpnfval  22313  deg1ldg  22470  deg1leb  22473  deg1val  22474  deg1valOLD  22475  deg1mul3  22494  deg1mul3le  22495  uc1pmon1p  22530  plyval  22568  elply2  22571  plyf  22573  elplyr  22576  plyeq0lem  22585  plyeq0  22586  plypf1  22587  plyaddlem1  22588  plyaddlem  22590  plymullem  22591  coeeulem  22599  coeeq  22602  dgrlem  22604  coeidlem  22612  coeaddlem  22624  coemulc  22630  coe0  22631  coesub  22632  dgradd2  22643  dgrcolem2  22649  plydivlem4  22670  plydiveu  22672  vieta1lem2  22685  taylfval  22732  pserval  22783  dvradcnv  22794  pserdvlem2  22801  abelthlem1  22804  abelthlem3  22806  abelthlem6  22809  logtayl  23019  leibpi  23251  sqff1o  23434  wwlkn  24660  clwwlkn  24745  clwwlknprop  24750  iseupa  24943  eulerpartleme  28280  eulerpartlem1  28284  eulerpartlemt  28288  eulerpartgbij  28289  eulerpartlemr  28291  eulerpartlemmf  28292  eulerpartlemgvv  28293  eulerpartlemgs2  28297  eulerpartlemn  28298  fib0  28316  fib1  28317  fibp1  28318  dfrtrclrec2  29044  rtrclreclem.refl  29045  rtrclreclem.subset  29046  rtrclreclem.min  29048  bpolylem  29786  heiborlem3  30285  eldiophb  30666  diophrw  30668  hbtlem1  31048  hbtlem7  31050  dgrsub2  31060  mpaaeu  31075  deg1mhm  31143  radcnvrat  31171  expfac  31617  dvnprodlem1  31697  dvnprodlem2  31698  dvnprodlem3  31699  etransclem24  31995  etransclem25  31996  etransclem26  31997  etransclem28  31999  etransclem35  32006  etransclem37  32008  etransclem48  32019  ply1mulgsum  32860
  Copyright terms: Public domain W3C validator