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

Theorem c0ex 9586
Description: 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
c0ex  |-  0  e.  _V

Proof of Theorem c0ex
StepHypRef Expression
1 0cn 9584 . 2  |-  0  e.  CC
21elexi 3123 1  |-  0  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1767   _Vcvv 3113   CCcc 9486   0cc0 9488
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-12 1803  ax-ext 2445  ax-1cn 9546  ax-icn 9547  ax-addcl 9548  ax-mulcl 9550  ax-i2m1 9556
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-v 3115
This theorem is referenced by:  ofsubeq0  10529  ofsubge0  10531  elnn0  10793  un0mulcl  10826  frnnn0supp  10845  frnnn0fsupp  10847  nn0ssz  10881  nn0ind-raph  10957  xaddval  11418  xmulval  11420  ser0f  12123  facnn  12317  fac0  12318  bcval  12344  snopiswrd  12516  wrdexb  12518  repsw1  12712  cshw1  12747  s1co  12756  wrdlen2i  12841  wrd2pr2op  12842  wwlktovf1  12852  sgnval  12878  iserge0  13439  sum0  13499  sumz  13500  fsumss  13503  fsumser  13508  isumless  13613  geomulcvg  13641  rpnnen2lem1  13802  ruclem4  13821  ruclem8  13824  0bits  13941  gcdval  13998  prmreclem2  14287  prmreclem5  14290  vdwapun  14344  odval  16351  odf  16354  gexval  16391  telgsumfz0  16809  telgsum  16811  srgbinom  16981  abvtrivd  17269  snifpsrbag  17783  psrbaglesupp  17785  psrbagaddcl  17788  psrbaglefi  17791  mplcoe5  17899  mplbas2  17902  ltbwe  17905  psrbag0  17927  psrbagev1  17945  cply1coe0bi  18110  m2cpminvid2lem  19019  pmatcollpw3fi1lem1  19051  pmatcollpw3fi1lem2  19052  pmatcollpw3fi1  19053  idpm2idmp  19066  prdsdsf  20602  prdsxmetlem  20603  prdsmet  20605  imasdsf1olem  20608  prdsbl  20726  xrge0gsumle  21070  xrge0tsms  21071  xrhmeo  21178  pcopt  21254  pcopt2  21255  pcoass  21256  rrxcph  21556  ovoliunnul  21650  ovolicc1  21659  vitalilem5  21753  mbfpos  21790  0pval  21810  0pledm  21812  i1f1lem  21828  i1f1  21829  itg11  21830  itg1addlem3  21837  itg1addlem4  21838  i1fres  21844  itg1climres  21853  mbfi1fseqlem4  21857  mbfi1fseqlem6  21859  mbfi1flimlem  21861  mbfi1flim  21862  xrge0f  21870  itg2ge0  21874  itg2uba  21882  itg2splitlem  21887  itg2monolem1  21889  itg2gt0  21899  itg2cnlem1  21900  ibl0  21925  i1fibl  21946  itgeqa  21952  itgcn  21981  dvcmul  22079  dvcmulf  22080  dvexp3  22111  rolle  22123  dveq0  22133  dv11cn  22134  tdeglem4  22190  elply2  22325  elplyd  22331  ply1term  22333  ply0  22337  plyeq0  22340  plypf1  22341  plymullem  22345  dgrlt  22394  plymul0or  22408  dvply1  22411  plydivlem4  22423  elqaalem2  22447  aareccl  22453  aannenlem2  22456  tayl0  22488  taylpfval  22491  dvtaylp  22496  pserdvlem2  22554  abelthlem9  22566  logtayl  22766  leibpilem2  22997  leibpi  22998  jensenlem2  23042  jensen  23043  amgmlem  23044  amgm  23045  vmaval  23112  vmaf  23118  muval  23131  dchrelbas2  23237  dchrinvcl  23253  dchrptlem2  23265  lgseisenlem4  23352  pntrlog2bndlem4  23490  pntrlog2bndlem5  23491  padicval  23527  padicabv  23540  ostth1  23543  axlowdimlem8  23925  axlowdimlem9  23926  axlowdimlem10  23927  axlowdimlem11  23928  axlowdimlem12  23929  axlowdimlem13  23930  axlowdimlem17  23934  2trllemA  24225  2trllemH  24227  2trllemE  24228  2wlklemA  24229  wlkntrllem1  24234  wlkntrllem2  24235  wlkntrllem3  24236  2wlklem  24239  0spth  24246  constr1trl  24263  1pthon  24266  2pthlem2  24271  2wlklem1  24272  2pthon  24277  2pthon3v  24279  usgra2adedgwlkonALT  24289  usgra2wlkspthlem1  24292  usgra2wlkspthlem2  24293  constr3lem2  24319  constr3lem4  24320  constr3lem5  24321  constr3trllem1  24323  constr3trllem2  24324  clwwlkn2  24448  usg2wlkonot  24556  usg2wotspth  24557  0egra0rgra  24609  rusgranumwlkl1  24620  eupath  24654  occllem  25894  0cnfn  26572  0lnfn  26577  nmfn0  26579  nmcexi  26618  nlelchi  26653  sgnsval  27377  sgnsf  27378  xrge0tsmsd  27435  xrge0iif1  27553  xrge0mulc1cn  27556  gsumesum  27704  esumpfinval  27718  esumpfinvalf  27719  ddeval1  27843  ddeval0  27844  eulerpartlemt  27947  coinfliprv  28058  sgncl  28114  plymul02  28140  plymulx  28142  signsw0glem  28147  signsw0g  28150  signswmnd  28151  signswrid  28152  signstfvn  28163  igamval  28226  cvmliftlem4  28370  cvmliftlem5  28371  relexp0  28524  mblfinlem2  29627  mblfinlem3  29628  ismblfin  29630  itg2addnclem  29641  itg2addnclem3  29643  itg2addnc  29644  ftc1anclem3  29667  ftc1anclem5  29669  ftc1anclem7  29671  ftc1anclem8  29672  ftc1anc  29673  dvacos  29679  prdsbnd  29890  heiborlem10  29917  diophrw  30294  monotoddzzfi  30480  zindbi  30484  mncn0  30693  aaitgo  30716  flcidc  30728  lcmval  30798  ofsubid  30829  lhe4.4ex1a  30834  dvsconst  30835  dvconstbi  30839  climrec  31145  stoweidlem55  31355  usgra2pthspth  31820  usgra2pthlem1  31822  usgra2pth  31823  usgra2adedglem1  31825  zlmodzxzel  32008  zlmodzxz0  32009  zlmodzxzscm  32010  zlmodzxzadd  32011  zlmodzxznm  32179  zlmodzxzldeplem  32180  zlmodzxzldeplem2  32183  ex-gt  32203  ex-gte  32204  renegclALT  33766
  Copyright terms: Public domain W3C validator