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

Theorem nn0ex 10801
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 10796 . 2  |-  NN0  =  ( NN  u.  { 0 } )
2 nnex 10542 . . 3  |-  NN  e.  _V
3 snex 4688 . . 3  |-  { 0 }  e.  _V
42, 3unex 6582 . 2  |-  ( NN  u.  { 0 } )  e.  _V
51, 4eqeltri 2551 1  |-  NN0  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1767   _Vcvv 3113    u. cun 3474   {csn 4027   0cc0 9492   NNcn 10536   NN0cn0 10795
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576  ax-cnex 9548  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-i2m1 9560  ax-1ne0 9561  ax-rrecex 9564  ax-cnre 9565
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-ov 6287  df-om 6685  df-recs 7042  df-rdg 7076  df-nn 10537  df-n0 10796
This theorem is referenced by:  nn0ennn  12057  nnenom  12058  fsuppmapnn0fiub0  12067  suppssfz  12068  fsuppmapnn0ub  12069  mptnn0fsupp  12071  mptnn0fsuppr  12073  elovmptnn0wrd  12549  expcnv  13638  geolim  13642  cvgrat  13655  mertenslem2  13657  eftlub  13705  bitsfval  13932  bitsf  13936  sadfval  13961  smufval  13986  smupf  13987  1arith  14304  ramcl  14406  fsfnn0gsumfsffz  16814  gsummptnn0fz  16817  psrbag  17812  coe1fval  18043  fvcoe1  18045  coe1fval3  18046  coe1f2  18047  coe1sfi  18051  coe1sfiOLD  18052  coe1fsupp  18053  00ply1bas  18080  ply1plusgfvi  18082  coe1z  18103  coe1add  18104  coe1addfv  18105  coe1mul2lem1  18107  coe1mul2lem2  18108  coe1mul2  18109  coe1tm  18113  coe1sclmul  18122  coe1sclmulfv  18123  coe1sclmul2  18124  ply1coefsupp  18135  ply1coe  18136  ply1coeOLD  18137  gsumsmonply1  18144  gsummoncoe1  18145  evls1gsumadd  18160  evls1gsummul  18161  evl1gsummul  18195  nn0srg  18282  pmatcollpw1  19072  pmatcollpw2lem  19073  pmatcollpw2  19074  pmatcollpw3lem  19079  pm2mpcl  19093  idpm2idmp  19097  mply1topmatcllem  19099  mply1topmatcl  19101  mp2pm2mplem2  19103  mp2pm2mplem5  19106  mp2pm2mp  19107  pm2mpghmlem2  19108  pm2mpghm  19112  pm2mpmhmlem2  19115  monmat2matmon  19120  pm2mp  19121  chfacfscmulgsum  19156  chfacfpmmulgsum  19160  cpmidpmatlem2  19167  cpmadumatpolylem1  19177  cpmadumatpolylem2  19178  chcoeffeqlem  19181  cayhamlem3  19183  cayhamlem4  19184  dyadmax  21770  cpnfval  22098  deg1ldg  22255  deg1leb  22258  deg1val  22259  deg1valOLD  22260  deg1mul3  22279  deg1mul3le  22280  uc1pmon1p  22315  plyval  22353  elply2  22356  plyf  22358  elplyr  22361  plyeq0lem  22370  plyeq0  22371  plypf1  22372  plyaddlem1  22373  plyaddlem  22375  plymullem  22376  coeeulem  22384  coeeq  22387  dgrlem  22389  coeidlem  22397  coeaddlem  22408  coemulc  22414  coe0  22415  coesub  22416  dgradd2  22427  dgrcolem2  22433  plydivlem4  22454  plydiveu  22456  vieta1lem2  22469  taylfval  22516  pserval  22567  dvradcnv  22578  pserdvlem2  22585  abelthlem1  22588  abelthlem3  22590  abelthlem6  22593  logtayl  22797  leibpi  23029  sqff1o  23212  wwlkn  24386  clwwlkn  24471  clwwlknprop  24476  iseupa  24669  eulerpartleme  27970  eulerpartlem1  27974  eulerpartlemt  27978  eulerpartgbij  27979  eulerpartlemr  27981  eulerpartlemmf  27982  eulerpartlemgvv  27983  eulerpartlemgs2  27987  eulerpartlemn  27988  fib0  28006  fib1  28007  fibp1  28008  dfrtrclrec2  28569  rtrclreclem.refl  28570  rtrclreclem.subset  28571  rtrclreclem.min  28573  bpolylem  29415  heiborlem3  29940  eldiophb  30322  diophrw  30324  hbtlem1  30704  hbtlem7  30706  dgrsub2  30716  mpaaeu  30732  deg1mhm  30800  ply1mulgsum  32089
  Copyright terms: Public domain W3C validator