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

Theorem nn0ex 11336
Description: The set of nonnegative integers exists. (Contributed by NM, 18-Jul-2004.)
Assertion
Ref Expression
nn0ex 0 ∈ V

Proof of Theorem nn0ex
StepHypRef Expression
1 df-n0 11331 . 2 0 = (ℕ ∪ {0})
2 nnex 11064 . . 3 ℕ ∈ V
3 snex 4938 . . 3 {0} ∈ V
42, 3unex 6998 . 2 (ℕ ∪ {0}) ∈ V
51, 4eqeltri 2726 1 0 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  Vcvv 3231  cun 3605  {csn 4210  0cc0 9974  cn 11058  0cn0 11330
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-i2m1 10042  ax-1ne0 10043  ax-rrecex 10046  ax-cnre 10047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-om 7108  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-nn 11059  df-n0 11331
This theorem is referenced by:  nn0ennn  12818  nnenom  12819  fsuppmapnn0fiub0  12833  suppssfz  12834  fsuppmapnn0ub  12835  mptnn0fsupp  12837  mptnn0fsuppr  12839  elovmptnn0wrd  13381  dfrtrclrec2  13841  rtrclreclem1  13842  rtrclreclem2  13843  rtrclreclem4  13845  expcnv  14640  geolim  14645  cvgrat  14659  mertenslem2  14661  bpolylem  14823  eftlub  14883  bitsfval  15192  bitsf  15196  sadfval  15221  smufval  15246  smupf  15247  1arith  15678  ramcl  15780  fsfnn0gsumfsffz  18425  gsummptnn0fz  18428  psrbag  19412  coe1fval  19623  fvcoe1  19625  coe1fval3  19626  coe1f2  19627  coe1sfi  19631  coe1fsupp  19632  00ply1bas  19658  ply1plusgfvi  19660  coe1z  19681  coe1add  19682  coe1addfv  19683  coe1mul2lem1  19685  coe1mul2lem2  19686  coe1mul2  19687  coe1tm  19691  coe1sclmul  19700  coe1sclmulfv  19701  coe1sclmul2  19702  ply1coefsupp  19713  ply1coe  19714  gsumsmonply1  19721  gsummoncoe1  19722  evls1gsumadd  19737  evls1gsummul  19738  evl1gsummul  19772  nn0srg  19864  pmatcollpw1  20629  pmatcollpw2lem  20630  pmatcollpw2  20631  pmatcollpw3lem  20636  pm2mpcl  20650  idpm2idmp  20654  mply1topmatcllem  20656  mply1topmatcl  20658  mp2pm2mplem2  20660  mp2pm2mplem5  20663  mp2pm2mp  20664  pm2mpghmlem2  20665  pm2mpghm  20669  pm2mpmhmlem2  20672  monmat2matmon  20677  pm2mp  20678  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  cpmidpmatlem2  20724  cpmadumatpolylem1  20734  cpmadumatpolylem2  20735  chcoeffeqlem  20738  cayhamlem3  20740  cayhamlem4  20741  dyadmax  23412  cpnfval  23740  deg1ldg  23897  deg1leb  23900  deg1val  23901  deg1mul3  23920  deg1mul3le  23921  uc1pmon1p  23956  plyval  23994  elply2  23997  plyf  23999  elplyr  24002  plyeq0lem  24011  plyeq0  24012  plypf1  24013  plyaddlem1  24014  plyaddlem  24016  plymullem  24017  coeeulem  24025  coeeq  24028  dgrlem  24030  coeidlem  24038  coeaddlem  24050  coemulc  24056  coe0  24057  coesub  24058  dgradd2  24069  dgrcolem2  24075  plydivlem4  24096  plydiveu  24098  vieta1lem2  24111  taylfval  24158  pserval  24209  dvradcnv  24220  pserdvlem2  24227  abelthlem1  24230  abelthlem3  24232  abelthlem6  24235  logtayl  24451  leibpi  24714  sqff1o  24953  clwwlknonmpt2  27062  eulerpartleme  30553  eulerpartlem1  30557  eulerpartlemt  30561  eulerpartgbij  30562  eulerpartlemr  30564  eulerpartlemmf  30565  eulerpartlemgvv  30566  eulerpartlemgs2  30570  eulerpartlemn  30571  fib0  30589  fib1  30590  fibp1  30591  knoppcnlem1  32608  knoppcnlem6  32613  poimirlem32  33571  heiborlem3  33742  eldiophb  37637  diophrw  37639  hbtlem1  38010  hbtlem7  38012  dgrsub2  38022  mpaaeu  38037  deg1mhm  38102  elrtrclrec  38290  brmptiunrelexpd  38292  brrtrclrec  38306  iunrelexp0  38311  iunrelexpmin2  38321  dfrtrcl3  38342  fvrtrcllb0d  38344  fvrtrcllb0da  38345  fvrtrcllb1d  38346  radcnvrat  38830  binomcxplemrat  38866  binomcxplemnotnn0  38872  expfac  40207  dvnprodlem1  40479  dvnprodlem2  40480  dvnprodlem3  40481  etransclem24  40793  etransclem25  40794  etransclem26  40795  etransclem28  40797  etransclem35  40804  etransclem37  40806  etransclem48  40817  fmtnoinf  41773  ply1mulgsum  42503
  Copyright terms: Public domain W3C validator