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

Theorem nn0ex 10695
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 10690 . 2  |-  NN0  =  ( NN  u.  { 0 } )
2 nnex 10438 . . 3  |-  NN  e.  _V
3 snex 4640 . . 3  |-  { 0 }  e.  _V
42, 3unex 6487 . 2  |-  ( NN  u.  { 0 } )  e.  _V
51, 4eqeltri 2538 1  |-  NN0  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1758   _Vcvv 3076    u. cun 3433   {csn 3984   0cc0 9392   NNcn 10432   NN0cn0 10689
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481  ax-cnex 9448  ax-resscn 9449  ax-1cn 9450  ax-icn 9451  ax-addcl 9452  ax-addrcl 9453  ax-mulcl 9454  ax-mulrcl 9455  ax-i2m1 9460  ax-1ne0 9461  ax-rrecex 9464  ax-cnre 9465
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-reu 2805  df-rab 2807  df-v 3078  df-sbc 3293  df-csb 3395  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-pss 3451  df-nul 3745  df-if 3899  df-pw 3969  df-sn 3985  df-pr 3987  df-tp 3989  df-op 3991  df-uni 4199  df-iun 4280  df-br 4400  df-opab 4458  df-mpt 4459  df-tr 4493  df-eprel 4739  df-id 4743  df-po 4748  df-so 4749  df-fr 4786  df-we 4788  df-ord 4829  df-on 4830  df-lim 4831  df-suc 4832  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-ov 6202  df-om 6586  df-recs 6941  df-rdg 6975  df-nn 10433  df-n0 10690
This theorem is referenced by:  nn0ennn  11917  nnenom  11918  expcnv  13443  geolim  13447  cvgrat  13460  mertenslem2  13462  eftlub  13510  bitsfval  13736  bitsf  13740  sadfval  13765  smufval  13790  smupf  13791  1arith  14105  ramcl  14207  psrbag  17553  coe1fval  17784  fvcoe1  17786  coe1fval3  17787  coe1f2  17788  coe1sfi  17791  coe1sfiOLD  17792  00ply1bas  17817  ply1plusgfvi  17819  coe1z  17839  coe1add  17840  coe1addfv  17841  coe1mul2lem1  17843  coe1mul2lem2  17844  coe1mul2  17845  coe1tm  17849  coe1sclmul  17858  coe1sclmulfv  17859  coe1sclmul2  17860  ply1coefsupp  17869  ply1coe  17870  ply1coeOLD  17871  evls1gsumadd  17883  evls1gsummul  17884  evl1gsummul  17918  nn0srg  18005  dyadmax  21210  cpnfval  21538  deg1ldg  21695  deg1leb  21698  deg1val  21699  deg1valOLD  21700  deg1mul3  21719  deg1mul3le  21720  uc1pmon1p  21755  plyval  21793  elply2  21796  plyf  21798  elplyr  21801  plyeq0lem  21810  plyeq0  21811  plypf1  21812  plyaddlem1  21813  plyaddlem  21815  plymullem  21816  coeeulem  21824  coeeq  21827  dgrlem  21829  coeidlem  21837  coeaddlem  21848  coemulc  21854  coe0  21855  coesub  21856  dgradd2  21867  dgrcolem2  21873  plydivlem4  21894  plydiveu  21896  vieta1lem2  21909  taylfval  21956  pserval  22007  dvradcnv  22018  pserdvlem2  22025  abelthlem1  22028  abelthlem3  22030  abelthlem6  22033  logtayl  22237  leibpi  22469  sqff1o  22652  iseupa  23737  eulerpartleme  26889  eulerpartlem1  26893  eulerpartlemt  26897  eulerpartgbij  26898  eulerpartlemr  26900  eulerpartlemmf  26901  eulerpartlemgvv  26902  eulerpartlemgs2  26906  eulerpartlemn  26907  fib0  26925  fib1  26926  fibp1  26927  dfrtrclrec2  27488  rtrclreclem.refl  27489  rtrclreclem.subset  27490  rtrclreclem.min  27492  bpolylem  28334  heiborlem3  28859  eldiophb  29242  diophrw  29244  hbtlem1  29626  hbtlem7  29628  dgrsub2  29638  mpaaeu  29654  deg1mhm  29722  elovmptnn0wrd  30404  wwlkn  30463  clwwlkn  30577  clwwlknprop  30582  suppssfz  30933  fsuppmapnn0ub  30943  fsuppmapnn0fiub0  30948  mptnn0fsupp  30949  mptnn0fsuppr  30951  fsfnn0gsumfsffz  30954  gsummptnn0fz  30957  coe1fsupp  30983  gsumsmonply1  30994  gsummoncoe1  30995  ply1mulgsum  31001  pmatcollpw1  31249  pmatcollpw2lem  31250  pmatcollpw2  31251  pmatcollpw3  31256  pm2mpcl  31269  idpm2idmp  31273  mply1topmatcllem  31275  mply1topmatcl  31277  mp2pm2mplem2  31279  mp2pm2mplem5  31282  mp2pm2mp  31283  pm2mpghmlem2  31284  pm2mpghm  31288  pm2mpmhmlem2  31291  monmat2matmon  31295  pm2mp  31296  chfacfscmulgsum  31331  chfacfpmmulgsum  31335  cpmidpmatlem2  31342  cpmadumatpolylem1  31352  cpmadumatpolylem3  31354  chcoeffeqlem  31357  cayhamlem3  31359  cayhamlem4  31360
  Copyright terms: Public domain W3C validator