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

Theorem nn0ex 10718
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 10713 . 2  |-  NN0  =  ( NN  u.  { 0 } )
2 nnex 10458 . . 3  |-  NN  e.  _V
3 snex 4603 . . 3  |-  { 0 }  e.  _V
42, 3unex 6497 . 2  |-  ( NN  u.  { 0 } )  e.  _V
51, 4eqeltri 2466 1  |-  NN0  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1826   _Vcvv 3034    u. cun 3387   {csn 3944   0cc0 9403   NNcn 10452   NN0cn0 10712
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491  ax-cnex 9459  ax-resscn 9460  ax-1cn 9461  ax-icn 9462  ax-addcl 9463  ax-addrcl 9464  ax-mulcl 9465  ax-mulrcl 9466  ax-i2m1 9471  ax-1ne0 9472  ax-rrecex 9475  ax-cnre 9476
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-reu 2739  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-pss 3405  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-tp 3949  df-op 3951  df-uni 4164  df-iun 4245  df-br 4368  df-opab 4426  df-mpt 4427  df-tr 4461  df-eprel 4705  df-id 4709  df-po 4714  df-so 4715  df-fr 4752  df-we 4754  df-ord 4795  df-on 4796  df-lim 4797  df-suc 4798  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-ov 6199  df-om 6600  df-recs 6960  df-rdg 6994  df-nn 10453  df-n0 10713
This theorem is referenced by:  nn0ennn  11992  nnenom  11993  fsuppmapnn0fiub0  12002  suppssfz  12003  fsuppmapnn0ub  12004  mptnn0fsupp  12006  mptnn0fsuppr  12008  elovmptnn0wrd  12492  dfrtrclrec2  12892  rtrclreclem1  12893  rtrclreclem2  12894  rtrclreclem4  12896  expcnv  13677  geolim  13681  cvgrat  13694  mertenslem2  13696  eftlub  13846  bitsfval  14075  bitsf  14079  sadfval  14104  smufval  14129  smupf  14130  1arith  14447  ramcl  14549  fsfnn0gsumfsffz  17124  gsummptnn0fz  17127  psrbag  18126  coe1fval  18357  fvcoe1  18359  coe1fval3  18360  coe1f2  18361  coe1sfi  18365  coe1sfiOLD  18366  coe1fsupp  18367  00ply1bas  18394  ply1plusgfvi  18396  coe1z  18417  coe1add  18418  coe1addfv  18419  coe1mul2lem1  18421  coe1mul2lem2  18422  coe1mul2  18423  coe1tm  18427  coe1sclmul  18436  coe1sclmulfv  18437  coe1sclmul2  18438  ply1coefsupp  18449  ply1coe  18450  ply1coeOLD  18451  gsumsmonply1  18458  gsummoncoe1  18459  evls1gsumadd  18474  evls1gsummul  18475  evl1gsummul  18509  nn0srg  18599  pmatcollpw1  19362  pmatcollpw2lem  19363  pmatcollpw2  19364  pmatcollpw3lem  19369  pm2mpcl  19383  idpm2idmp  19387  mply1topmatcllem  19389  mply1topmatcl  19391  mp2pm2mplem2  19393  mp2pm2mplem5  19396  mp2pm2mp  19397  pm2mpghmlem2  19398  pm2mpghm  19402  pm2mpmhmlem2  19405  monmat2matmon  19410  pm2mp  19411  chfacfscmulgsum  19446  chfacfpmmulgsum  19450  cpmidpmatlem2  19457  cpmadumatpolylem1  19467  cpmadumatpolylem2  19468  chcoeffeqlem  19471  cayhamlem3  19473  cayhamlem4  19474  dyadmax  22092  cpnfval  22420  deg1ldg  22577  deg1leb  22580  deg1val  22581  deg1valOLD  22582  deg1mul3  22601  deg1mul3le  22602  uc1pmon1p  22637  plyval  22675  elply2  22678  plyf  22680  elplyr  22683  plyeq0lem  22692  plyeq0  22693  plypf1  22694  plyaddlem1  22695  plyaddlem  22697  plymullem  22698  coeeulem  22706  coeeq  22709  dgrlem  22711  coeidlem  22719  coeaddlem  22731  coemulc  22737  coe0  22738  coesub  22739  dgradd2  22750  dgrcolem2  22756  plydivlem4  22777  plydiveu  22779  vieta1lem2  22792  taylfval  22839  pserval  22890  dvradcnv  22901  pserdvlem2  22908  abelthlem1  22911  abelthlem3  22913  abelthlem6  22916  logtayl  23128  leibpi  23389  sqff1o  23573  wwlkn  24803  clwwlkn  24888  clwwlknprop  24893  iseupa  25086  eulerpartleme  28485  eulerpartlem1  28489  eulerpartlemt  28493  eulerpartgbij  28494  eulerpartlemr  28496  eulerpartlemmf  28497  eulerpartlemgvv  28498  eulerpartlemgs2  28502  eulerpartlemn  28503  fib0  28521  fib1  28522  fibp1  28523  bpolylem  29963  heiborlem3  30475  eldiophb  30855  diophrw  30857  hbtlem1  31240  hbtlem7  31242  dgrsub2  31252  mpaaeu  31267  deg1mhm  31335  radcnvrat  31363  binomcxplemrat  31423  binomcxplemnotnn0  31429  expfac  31829  dvnprodlem1  31909  dvnprodlem2  31910  dvnprodlem3  31911  etransclem24  32207  etransclem25  32208  etransclem26  32209  etransclem28  32211  etransclem35  32218  etransclem37  32220  etransclem48  32231  ply1mulgsum  33190  iunrelexpmin2  38226  elrtrclrec  38229  brrtrclrec  38230  dfrtrcl3  38232  iunrelexp0  38242
  Copyright terms: Public domain W3C validator