Theorem c0ex 10962

Description: Zero is a set. (Contributed by David A. Wheeler, 7-Jul-2016.)

Assertion

Ref	Expression
c0ex	⊢ 0 ∈ V

Proof of Theorem c0ex

Step	Hyp	Ref	Expression
1		0cn 10960	. 2 ⊢ 0 ∈ ℂ
2	1	elexi 3450	1 ⊢ 0 ∈ V

Syntax hints:   ∈ wcel 2110  Vcvv 3431  ℂcc 10862  0cc0 10864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711  ax-1cn 10922  ax-icn 10923  ax-addcl 10924  ax-mulcl 10926  ax-i2m1 10932

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433

This theorem is referenced by:  ofsubeq0  11962  ofsubge0  11964  elnn0  12227  un0mulcl  12259  frnnn0supp  12281  frnnn0fsupp  12282  frnnn0suppg  12283  frnnn0fsuppg  12284  nn0ssz  12333  nn0ind-raph  12412  xaddval  12948  xmulval  12950  ser0f  13766  facnn  13979  fac0  13980  bcval  14008  prhash2ex  14104  wrdexb  14218  s1rn  14294  eqs1  14307  repsw1  14486  cshw1  14525  s1co  14536  funcnvs2  14616  funcnvs3  14617  funcnvs4  14618  wrdlen2i  14645  wrd2pr2op  14646  wrd3tpop  14651  wwlktovf1  14662  wrdl3s3  14667  sgnval  14789  iserge0  15362  sum0  15423  sumz  15424  fsumss  15427  fsumser  15432  isumless  15547  geomulcvg  15578  rpnnen2lem1  15913  ruclem4  15933  ruclem8  15936  ruclem11  15939  0bits  16136  gcdval  16193  lcmval  16287  lcmfpr  16322  lcmfunsnlem2  16335  prmreclem2  16608  prmreclem5  16611  vdwapun  16665  smndex1n0mnd  18541  mgmnsgrpex  18560  odval  19132  odf  19135  gexval  19173  telgsumfz0  19583  telgsum  19585  srgbinom  19771  abvtrivd  20090  snifpsrbag  21115  psrbaglesupp  21117  psrbaglesuppOLD  21118  psrbagaddclOLD  21122  psrbaglefi  21125  psrbaglefiOLD  21126  mplcoe5  21231  mplbas2  21233  ltbwe  21235  psrbag0  21260  psrbagev1  21275  psrbagev1OLD  21276  mhpmulcl  21329  cply1coe0bi  21461  m2cpminvid2lem  21893  pmatcollpw3fi1lem1  21925  pmatcollpw3fi1lem2  21926  pmatcollpw3fi1  21927  idpm2idmp  21940  prdsdsf  23510  prdsxmetlem  23511  prdsmet  23513  imasdsf1olem  23516  prdsbl  23637  xrge0gsumle  23986  xrge0tsms  23987  xrhmeo  24099  pcopt  24175  pcopt2  24176  pcoass  24177  rrxcph  24546  rrx0el  24552  rrxbasefi  24564  ovoliunnul  24661  ovolicc1  24670  vitalilem5  24766  mbfpos  24805  0pval  24825  0pledm  24827  i1f1lem  24843  i1f1  24844  itg11  24845  itg1addlem3  24852  itg1addlem4  24853  itg1addlem4OLD  24854  i1fres  24860  itg1climres  24869  mbfi1fseqlem4  24873  mbfi1fseqlem6  24875  mbfi1flimlem  24877  mbfi1flim  24878  xrge0f  24886  itg2ge0  24890  itg2uba  24898  itg2splitlem  24903  itg2monolem1  24905  itg2gt0  24915  itg2cnlem1  24916  ibl0  24941  iblcnlem1  24942  i1fibl  24962  itgeqa  24968  itgcn  24999  dvcmul  25098  dvcmulf  25099  dvexp3  25132  dvef  25134  rolle  25144  dveq0  25154  dv11cn  25155  tdeglem4  25214  tdeglem4OLD  25215  elply2  25347  elplyd  25353  ply1term  25355  ply0  25359  plyeq0  25362  plypf1  25363  plymullem  25367  dgrlt  25417  plymul0or  25431  dvply1  25434  plydivlem4  25446  elqaalem2  25470  iaa  25475  aareccl  25476  aannenlem2  25479  tayl0  25511  taylpfval  25514  dvtaylp  25519  pserdvlem2  25577  abelthlem9  25589  logtayl  25805  cxplogb  25926  leibpilem2  26081  leibpi  26082  jensenlem2  26127  jensen  26128  amgmlem  26129  amgm  26130  igamval  26186  vmaval  26252  vmaf  26258  muval  26271  dchrelbas2  26375  dchrinvcl  26391  dchrptlem2  26403  lgseisenlem4  26516  addsqnreup  26581  pntrlog2bndlem4  26718  pntrlog2bndlem5  26719  padicval  26755  padicabv  26768  ostth1  26771  axlowdimlem8  27307  axlowdimlem9  27308  axlowdimlem10  27309  axlowdimlem11  27310  axlowdimlem12  27311  axlowdimlem13  27312  axlowdimlem17  27316  uspgr1ewop  27605  usgr2v1e2w  27609  umgr2v2eedg  27881  umgr2v2e  27882  umgr2v2evd2  27884  wlkl1loop  27994  2wlklem  28024  usgr2trlncl  28116  2wlkdlem4  28281  2wlkdlem5  28282  2pthdlem1  28283  2wlkdlem10  28288  umgrwwlks2on  28310  rusgrnumwwlkl1  28321  clwwlkn2  28396  0spth  28478  1wlkdlem4  28492  wlk2v2elem1  28507  3wlkdlem4  28514  3wlkdlem5  28515  3pthdlem1  28516  3wlkdlem10  28521  upgr3v3e3cycl  28532  upgr4cycl4dv4e  28537  eulerpathpr  28592  konigsberglem4  28607  konigsberglem5  28608  wlkl0  28719  occllem  29653  0cnfn  30330  0lnfn  30335  nmfn0  30337  nmcexi  30376  nlelchi  30411  fprodex01  31127  s2rn  31206  s3rn  31208  xrge0tsmsd  31305  cyc2fv1  31376  cyc3fv1  31392  cyc3evpm  31405  sgnsval  31416  sgnsf  31417  xrge0iif1  31876  xrge0mulc1cn  31879  gsumesum  32015  esumpfinval  32031  esumpfinvalf  32032  ddeval1  32190  ddeval0  32191  ddemeas  32192  eulerpartlemt  32326  coinfliprv  32437  sgncl  32493  plymul02  32513  plymulx  32515  signsw0glem  32520  signsw0g  32523  signswmnd  32524  signswrid  32525  prodfzo03  32571  circlevma  32610  circlemethhgt  32611  hgt750lemg  32622  hgt750lemb  32624  hgt750lema  32625  hgt750leme  32626  tgoldbachgtde  32628  tgoldbachgt  32631  cvmliftlem4  33238  cvmliftlem5  33239  poimirlem1  35766  poimirlem2  35767  poimirlem3  35768  poimirlem4  35769  poimirlem5  35770  poimirlem6  35771  poimirlem7  35772  poimirlem11  35776  poimirlem12  35777  poimirlem16  35781  poimirlem17  35782  poimirlem19  35784  poimirlem20  35785  poimirlem22  35787  poimirlem23  35788  poimirlem24  35789  poimirlem25  35790  poimirlem28  35793  poimirlem29  35794  poimirlem31  35796  poimirlem32  35797  poimir  35798  broucube  35799  mblfinlem2  35803  mblfinlem3  35804  ismblfin  35806  itg2addnclem  35816  itg2addnclem3  35818  itg2addnc  35819  ftc1anclem3  35840  ftc1anclem5  35842  ftc1anclem7  35844  ftc1anclem8  35845  ftc1anc  35846  dvacos  35850  prdsbnd  35939  heiborlem10  35966  renegclALT  36965  aks4d1p1p4  40068  evlsbagval  40264  mhphf  40274  0prjspnlem  40449  0prjspnrel  40453  diophrw  40570  monotoddzzfi  40753  zindbi  40757  mncn0  40953  aaitgo  40976  flcidc  40988  dfrcl4  41246  fvrcllb0d  41263  fvrcllb0da  41264  iunrelexp0  41272  corclrcl  41277  relexp0idm  41285  dfrtrcl4  41308  corcltrcl  41309  cotrclrcl  41312  ofsubid  41904  lhe4.4ex1a  41909  dvsconst  41910  dvconstbi  41914  binomcxplemnn0  41929  binomcxplemdvbinom  41933  binomcxplemnotnn0  41936  n0p  42553  climrec  43107  limsup10exlem  43276  dvnmptdivc  43442  dvnmul  43447  stoweidlem55  43559  fourierdlem62  43672  fourierdlem104  43714  fouriersw  43735  ovnval2  44046  hoidmvval  44078  fun2dmnopgexmpl  44736  el1fzopredsuc  44778  nn0mnd  45334  zlmodzxzel  45652  zlmodzxz0  45653  zlmodzxzscm  45654  zlmodzxzadd  45655  zlmodzxznm  45799  zlmodzxzldeplem  45800  zlmodzxzldeplem2  45803  blen0  45879  nn0sumshdiglemB  45927  fv1arycl  45944  1arympt1  45945  1arympt1fv  45946  1arymaptf1  45949  1arymaptfo  45950  fv2arycl  45955  2arympt  45956  2arymptfv  45957  2arymaptf1  45960  2arymaptfo  45961  ehl2eudisval0  46032  2sphere0  46057  line2ylem  46058  line2  46059  line2x  46061  line2y  46062  ex-gt  46391  ex-gte  46392  aacllem  46466