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

Theorem nn0ex 10573
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 10568 . 2  |-  NN0  =  ( NN  u.  { 0 } )
2 nnex 10316 . . 3  |-  NN  e.  _V
3 snex 4521 . . 3  |-  { 0 }  e.  _V
42, 3unex 6367 . 2  |-  ( NN  u.  { 0 } )  e.  _V
51, 4eqeltri 2503 1  |-  NN0  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1755   _Vcvv 2962    u. cun 3314   {csn 3865   0cc0 9270   NNcn 10310   NN0cn0 10567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-cnex 9326  ax-resscn 9327  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-addrcl 9331  ax-mulcl 9332  ax-mulrcl 9333  ax-i2m1 9338  ax-1ne0 9339  ax-rrecex 9342  ax-cnre 9343
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-reu 2712  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-ov 6083  df-om 6466  df-recs 6818  df-rdg 6852  df-nn 10311  df-n0 10568
This theorem is referenced by:  nn0ennn  11785  nnenom  11786  expcnv  13309  geolim  13313  cvgrat  13326  mertenslem2  13328  eftlub  13376  bitsfval  13602  bitsf  13606  sadfval  13631  smufval  13656  smupf  13657  1arith  13971  ramcl  14073  psrbag  17365  coe1fval  17560  fvcoe1  17562  coe1fval3  17563  coe1f2  17564  coe1sfi  17567  coe1sfiOLD  17568  00ply1bas  17593  ply1plusgfvi  17595  coe1z  17615  coe1add  17616  coe1addfv  17617  coe1mul2lem1  17619  coe1mul2lem2  17620  coe1mul2  17621  coe1tm  17624  coe1sclmul  17633  coe1sclmulfv  17634  coe1sclmul2  17635  ply1coe  17643  dyadmax  20920  cpnfval  21248  deg1ldg  21448  deg1leb  21451  deg1val  21452  deg1valOLD  21453  deg1mul3  21472  deg1mul3le  21473  uc1pmon1p  21508  plyval  21546  elply2  21549  plyf  21551  elplyr  21554  plyeq0lem  21563  plyeq0  21564  plypf1  21565  plyaddlem1  21566  plyaddlem  21568  plymullem  21569  coeeulem  21577  coeeq  21580  dgrlem  21582  coeidlem  21590  coeaddlem  21601  coemulc  21607  coe0  21608  coesub  21609  dgradd2  21620  dgrcolem2  21626  plydivlem4  21647  plydiveu  21649  vieta1lem2  21662  taylfval  21709  pserval  21760  dvradcnv  21771  pserdvlem2  21778  abelthlem1  21781  abelthlem3  21783  abelthlem6  21786  logtayl  21990  leibpi  22222  sqff1o  22405  iseupa  23409  nn0srg  26063  eulerpartleme  26594  eulerpartlem1  26598  eulerpartlemt  26602  eulerpartgbij  26603  eulerpartlemr  26605  eulerpartlemmf  26606  eulerpartlemgvv  26607  eulerpartlemgs2  26611  eulerpartlemn  26612  fib0  26630  fib1  26631  fibp1  26632  dfrtrclrec2  27192  rtrclreclem.refl  27193  rtrclreclem.subset  27194  rtrclreclem.min  27196  bpolylem  28038  heiborlem3  28556  eldiophb  28940  diophrw  28942  hbtlem1  29324  hbtlem7  29326  dgrsub2  29336  mpaaeu  29352  deg1mhm  29420  elovmptnn0wrd  30103  wwlkn  30162  clwwlkn  30276  clwwlknprop  30281  ply1coefsupp  30634
  Copyright terms: Public domain W3C validator