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

Theorem c0ex 9913
Description: 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
c0ex 0 ∈ V

Proof of Theorem c0ex
StepHypRef Expression
1 0cn 9911 . 2 0 ∈ ℂ
21elexi 3186 1 0 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 1977  Vcvv 3173  cc 9813  0cc0 9815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-ext 2590  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-mulcl 9877  ax-i2m1 9883
This theorem depends on definitions:  df-bi 196  df-an 385  df-tru 1478  df-ex 1696  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175
This theorem is referenced by:  ofsubeq0  10894  ofsubge0  10896  elnn0  11171  un0mulcl  11204  frnnn0supp  11226  frnnn0fsupp  11227  nn0ssz  11275  nn0ind-raph  11353  xaddval  11928  xmulval  11930  ser0f  12716  facnn  12924  fac0  12925  bcval  12953  prhash2ex  13048  wrdexb  13171  s1rn  13232  eqs1  13245  repsw1  13381  cshw1  13419  s1co  13430  funcnvs2  13508  funcnvs3  13509  funcnvs4  13510  wrdlen2i  13534  wrd2pr2op  13535  wrd3tpop  13539  wwlktovf1  13548  wrdl3s3  13553  sgnval  13676  iserge0  14239  sum0  14299  sumz  14300  fsumss  14303  fsumser  14308  isumless  14416  geomulcvg  14446  rpnnen2lem1  14782  ruclem4  14802  ruclem8  14805  ruclem11  14808  0bits  14999  gcdval  15056  lcmval  15143  lcmfpr  15178  lcmfunsnlem2  15191  prmreclem2  15459  prmreclem5  15462  vdwapun  15516  mgmnsgrpex  17241  odval  17776  odf  17779  gexval  17816  telgsumfz0  18212  telgsum  18214  srgbinom  18368  abvtrivd  18663  snifpsrbag  19187  psrbaglesupp  19189  psrbagaddcl  19191  psrbaglefi  19193  mplcoe5  19289  mplbas2  19291  ltbwe  19293  psrbag0  19315  psrbagev1  19331  cply1coe0bi  19491  m2cpminvid2lem  20378  pmatcollpw3fi1lem1  20410  pmatcollpw3fi1lem2  20411  pmatcollpw3fi1  20412  idpm2idmp  20425  prdsdsf  21982  prdsxmetlem  21983  prdsmet  21985  imasdsf1olem  21988  prdsbl  22106  xrge0gsumle  22444  xrge0tsms  22445  xrhmeo  22553  pcopt  22630  pcopt2  22631  pcoass  22632  rrxcph  22988  ovoliunnul  23082  ovolicc1  23091  vitalilem5  23187  mbfpos  23224  0pval  23244  0pledm  23246  i1f1lem  23262  i1f1  23263  itg11  23264  itg1addlem3  23271  itg1addlem4  23272  i1fres  23278  itg1climres  23287  mbfi1fseqlem4  23291  mbfi1fseqlem6  23293  mbfi1flimlem  23295  mbfi1flim  23296  xrge0f  23304  itg2ge0  23308  itg2uba  23316  itg2splitlem  23321  itg2monolem1  23323  itg2gt0  23333  itg2cnlem1  23334  ibl0  23359  iblcnlem1  23360  i1fibl  23380  itgeqa  23386  itgcn  23415  dvcmul  23513  dvcmulf  23514  dvexp3  23545  rolle  23557  dveq0  23567  dv11cn  23568  tdeglem4  23624  elply2  23756  elplyd  23762  ply1term  23764  ply0  23768  plyeq0  23771  plypf1  23772  plymullem  23776  dgrlt  23826  plymul0or  23840  dvply1  23843  plydivlem4  23855  elqaalem2  23879  iaa  23884  aareccl  23885  aannenlem2  23888  tayl0  23920  taylpfval  23923  dvtaylp  23928  pserdvlem2  23986  abelthlem9  23998  logtayl  24206  cxplogb  24324  leibpilem2  24468  leibpi  24469  jensenlem2  24514  jensen  24515  amgmlem  24516  amgm  24517  igamval  24573  vmaval  24639  vmaf  24645  muval  24658  dchrelbas2  24762  dchrinvcl  24778  dchrptlem2  24790  lgseisenlem4  24903  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  padicval  25106  padicabv  25119  ostth1  25122  axlowdimlem8  25629  axlowdimlem9  25630  axlowdimlem10  25631  axlowdimlem11  25632  axlowdimlem12  25633  axlowdimlem13  25634  axlowdimlem17  25638  2trllemA  26080  2trllemH  26082  2trllemE  26083  2wlklemA  26084  wlkntrllem1  26089  wlkntrllem2  26090  wlkntrllem3  26091  2wlklem  26094  0spth  26101  constr1trl  26118  1pthon  26121  2pthlem2  26126  2wlklem1  26127  2pthon  26132  2pthon3v  26134  usgra2adedgwlkonALT  26144  usgra2wlkspthlem1  26147  usgra2wlkspthlem2  26148  constr3lem2  26174  constr3lem4  26175  constr3lem5  26176  constr3trllem1  26178  constr3trllem2  26179  clwwlkn2  26303  usg2wlkonot  26410  usg2wotspth  26411  0egra0rgra  26463  rusgranumwlkl1  26474  eupath  26508  occllem  27546  0cnfn  28223  0lnfn  28228  nmfn0  28230  nmcexi  28269  nlelchi  28304  sgnsval  29059  sgnsf  29060  xrge0tsmsd  29116  xrge0iif1  29312  xrge0mulc1cn  29315  gsumesum  29448  esumpfinval  29464  esumpfinvalf  29465  ddeval1  29624  ddeval0  29625  ddemeas  29626  eulerpartlemt  29760  coinfliprv  29871  sgncl  29927  plymul02  29949  plymulx  29951  signsw0glem  29956  signsw0g  29959  signswmnd  29960  signswrid  29961  signstfvn  29972  cvmliftlem4  30524  cvmliftlem5  30525  poimirlem1  32580  poimirlem2  32581  poimirlem3  32582  poimirlem4  32583  poimirlem5  32584  poimirlem6  32585  poimirlem7  32586  poimirlem11  32590  poimirlem12  32591  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem22  32601  poimirlem23  32602  poimirlem24  32603  poimirlem25  32604  poimirlem28  32607  poimirlem29  32608  poimirlem31  32610  poimirlem32  32611  poimir  32612  broucube  32613  mblfinlem2  32617  mblfinlem3  32618  ismblfin  32620  itg2addnclem  32631  itg2addnclem3  32633  itg2addnc  32634  ftc1anclem3  32657  ftc1anclem5  32659  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  dvacos  32667  prdsbnd  32762  heiborlem10  32789  renegclALT  33267  diophrw  36340  monotoddzzfi  36525  zindbi  36529  mncn0  36728  aaitgo  36751  flcidc  36763  dfrcl4  36987  fvrcllb0d  37004  fvrcllb0da  37005  iunrelexp0  37013  corclrcl  37018  relexp0idm  37026  dfrtrcl4  37049  corcltrcl  37050  cotrclrcl  37053  ofsubid  37545  lhe4.4ex1a  37550  dvsconst  37551  dvconstbi  37555  binomcxplemnn0  37570  binomcxplemdvbinom  37574  binomcxplemnotnn0  37577  n0p  38234  climrec  38670  dvnmptdivc  38828  dvnmul  38833  stoweidlem55  38948  fourierdlem62  39061  fourierdlem104  39103  fouriersw  39124  rrxbasefi  39179  ovnval2  39435  hoidmvval  39467  hoidmvlelem1  39485  el1fzopredsuc  39948  fun2dmnopgexmpl  40329  uspgr1ewop  40474  usgr2v1e2w  40478  umgr2v2eedg  40740  umgr2v2e  40741  umgr2v2evd2  40743  1wlkl1loop  40842  2Wlklem  40875  usgr2wlkneq  40962  usgr2trlncl  40966  21wlkdlem4  41135  21wlkdlem5  41136  2pthdlem1  41137  21wlkdlem10  41142  umgrwwlks2on  41161  rusgrnumwwlkl1  41172  clwwlksn2  41217  0spth-av  41294  11wlkdlem4  41307  1wlk2v2elem1  41322  31wlkdlem4  41329  31wlkdlem5  41330  3pthdlem1  41331  31wlkdlem10  41336  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352  eulerpathpr  41408  konigsberglem4  41425  konigsberglem5  41426  zlmodzxzel  41926  zlmodzxz0  41927  zlmodzxzscm  41928  zlmodzxzadd  41929  zlmodzxznm  42080  zlmodzxzldeplem  42081  zlmodzxzldeplem2  42084  blen0  42164  nn0sumshdiglemB  42212  ex-gt  42268  ex-gte  42269  aacllem  42356
  Copyright terms: Public domain W3C validator