Theorem c0ex 11103

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 11101	. 2 ⊢ 0 ∈ ℂ
2	1	elexi 3459	1 ⊢ 0 ∈ V

Syntax hints:   ∈ wcel 2111  Vcvv 3436  ℂcc 11001  0cc0 11003

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-1cn 11061  ax-icn 11062  ax-addcl 11063  ax-mulcl 11065  ax-i2m1 11071

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438

This theorem is referenced by:  ofsubeq0  12119  ofsubge0  12121  elnn0  12380  un0mulcl  12412  fcdmnn0supp  12435  fcdmnn0fsupp  12436  fcdmnn0suppg  12437  fcdmnn0fsuppg  12438  nn0ssz  12488  nn0ind-raph  12570  xaddval  13119  xmulval  13121  ser0f  13959  facnn  14179  fac0  14180  bcval  14208  prhash2ex  14303  wrdexb  14429  s1rn  14504  eqs1  14517  repsw1  14687  cshw1  14726  s1co  14737  funcnvs2  14817  funcnvs3  14818  funcnvs4  14819  wrdlen2i  14846  wrd2pr2op  14847  wrd3tpop  14852  wwlktovf1  14861  wrdl3s3  14866  sgnval  14992  iserge0  15565  sum0  15625  sumz  15626  fsumss  15629  fsumser  15634  isumless  15749  geomulcvg  15780  rpnnen2lem1  16120  ruclem4  16140  ruclem8  16143  ruclem11  16146  0bits  16347  gcdval  16404  lcmval  16500  lcmfpr  16535  lcmfunsnlem2  16548  prmreclem2  16826  prmreclem5  16829  vdwapun  16883  smndex1n0mnd  18817  mgmnsgrpex  18836  odval  19444  odf  19447  gexval  19488  telgsumfz0  19902  telgsum  19904  srgbinom  20147  abvtrivd  20745  pzriprnglem4  21419  pzriprnglem5  21420  pzriprnglem7  21422  pzriprnglem9  21424  pzriprnglem10  21425  snifpsrbag  21855  psrbaglesupp  21857  psrbaglefi  21861  mplcoe5  21973  mplbas2  21975  ltbwe  21977  psrbag0  21995  psrbagev1  22010  mhpmulcl  22062  psdmplcl  22075  psdmvr  22082  cply1coe0bi  22215  m2cpminvid2lem  22667  pmatcollpw3fi1lem1  22699  pmatcollpw3fi1lem2  22700  pmatcollpw3fi1  22701  idpm2idmp  22714  prdsdsf  24280  prdsxmetlem  24281  prdsmet  24283  imasdsf1olem  24286  prdsbl  24404  xrge0gsumle  24747  xrge0tsms  24748  xrhmeo  24869  pcopt  24947  pcopt2  24948  pcoass  24949  rrxcph  25317  rrx0el  25323  rrxbasefi  25335  ovoliunnul  25433  ovolicc1  25442  vitalilem5  25538  mbfpos  25577  0pval  25597  0pledm  25599  i1f1lem  25615  i1f1  25616  itg11  25617  itg1addlem3  25624  itg1addlem4  25625  i1fres  25631  itg1climres  25640  mbfi1fseqlem4  25644  mbfi1fseqlem6  25646  mbfi1flimlem  25648  mbfi1flim  25649  xrge0f  25657  itg2ge0  25661  itg2uba  25669  itg2splitlem  25674  itg2monolem1  25676  itg2gt0  25686  itg2cnlem1  25687  ibl0  25713  iblcnlem1  25714  i1fibl  25734  itgeqa  25740  itgcn  25771  dvcmul  25872  dvcmulf  25873  dvexp3  25907  dvef  25909  rolle  25919  dveq0  25930  dv11cn  25931  tdeglem4  25990  elply2  26126  elplyd  26132  ply1term  26134  ply0  26138  plyeq0  26141  plypf1  26142  plymullem  26146  dgrlt  26197  plymul0or  26213  dvply1  26216  plydivlem4  26229  elqaalem2  26253  iaa  26258  aareccl  26259  aannenlem2  26262  tayl0  26294  taylpfval  26297  dvtaylp  26303  pserdvlem2  26363  abelthlem9  26375  logtayl  26594  cxplogb  26721  leibpilem2  26876  leibpi  26877  jensenlem2  26923  jensen  26924  amgmlem  26925  amgm  26926  igamval  26982  vmaval  27048  vmaf  27054  muval  27067  dchrelbas2  27173  dchrinvcl  27189  dchrptlem2  27201  lgseisenlem4  27314  addsqnreup  27379  pntrlog2bndlem4  27516  pntrlog2bndlem5  27517  padicval  27553  padicabv  27566  ostth1  27569  axlowdimlem8  28925  axlowdimlem9  28926  axlowdimlem10  28927  axlowdimlem11  28928  axlowdimlem12  28929  axlowdimlem13  28930  axlowdimlem17  28934  uspgr1ewop  29224  usgr2v1e2w  29228  umgr2v2eedg  29501  umgr2v2e  29502  umgr2v2evd2  29504  wlkl1loop  29614  2wlklem  29642  usgr2trlncl  29736  2wlkdlem4  29904  2wlkdlem5  29905  2pthdlem1  29906  2wlkdlem10  29911  umgrwwlks2on  29933  rusgrnumwwlkl1  29944  clwwlkn2  30019  0spth  30101  1wlkdlem4  30115  wlk2v2elem1  30130  3wlkdlem4  30137  3wlkdlem5  30138  3pthdlem1  30139  3wlkdlem10  30144  upgr3v3e3cycl  30155  upgr4cycl4dv4e  30160  eulerpathpr  30215  konigsberglem4  30230  konigsberglem5  30231  wlkl0  30342  occllem  31278  0cnfn  31955  0lnfn  31960  nmfn0  31962  nmcexi  32001  nlelchi  32036  fprodex01  32803  sgncl  32809  indsupp  32843  indfsd  32844  indfsid  32845  s2rnOLD  32920  s3rnOLD  32922  xrge0tsmsd  33037  cyc2fv1  33085  cyc3fv1  33101  cyc3evpm  33114  sgnsval  33125  sgnsf  33126  elrgspnlem1  33204  elrgspnlem4  33207  gsumind  33305  esplysply  33587  constr01  33750  constrss  33751  constrconj  33753  constrextdg2lem  33756  nn0constr  33769  xrge0iif1  33946  xrge0mulc1cn  33949  gsumesum  34067  esumpfinval  34083  esumpfinvalf  34084  ddeval1  34242  ddeval0  34243  ddemeas  34244  eulerpartlemt  34379  coinfliprv  34491  plymul02  34554  plymulx  34556  signsw0glem  34561  signsw0g  34564  signswmnd  34565  signswrid  34566  prodfzo03  34611  circlevma  34650  circlemethhgt  34651  hgt750lemg  34662  hgt750lemb  34664  hgt750lema  34665  hgt750leme  34666  tgoldbachgtde  34668  tgoldbachgt  34671  cvmliftlem4  35320  cvmliftlem5  35321  poimirlem1  37660  poimirlem2  37661  poimirlem3  37662  poimirlem4  37663  poimirlem5  37664  poimirlem6  37665  poimirlem7  37666  poimirlem11  37670  poimirlem12  37671  poimirlem16  37675  poimirlem17  37676  poimirlem19  37678  poimirlem20  37679  poimirlem22  37681  poimirlem23  37682  poimirlem24  37683  poimirlem25  37684  poimirlem28  37687  poimirlem29  37688  poimirlem31  37690  poimirlem32  37691  poimir  37692  broucube  37693  mblfinlem2  37697  mblfinlem3  37698  ismblfin  37700  itg2addnclem  37710  itg2addnclem3  37712  itg2addnc  37713  ftc1anclem3  37734  ftc1anclem5  37736  ftc1anclem7  37738  ftc1anclem8  37739  ftc1anc  37740  dvacos  37744  prdsbnd  37832  heiborlem10  37859  renegclALT  39001  aks4d1p1p4  42103  aks6d1c7lem1  42212  0prjspnlem  42655  0prjspnrel  42659  diophrw  42791  monotoddzzfi  42974  zindbi  42978  mncn0  43171  aaitgo  43194  flcidc  43202  dfrcl4  43708  fvrcllb0d  43725  fvrcllb0da  43726  iunrelexp0  43734  corclrcl  43739  relexp0idm  43747  dfrtrcl4  43770  corcltrcl  43771  cotrclrcl  43774  ofsubid  44356  lhe4.4ex1a  44361  dvsconst  44362  dvconstbi  44366  binomcxplemnn0  44381  binomcxplemdvbinom  44385  binomcxplemnotnn0  44388  n0p  45081  climrec  45642  limsup10exlem  45809  dvnmptdivc  45975  dvnmul  45980  stoweidlem55  46092  fourierdlem62  46205  fourierdlem104  46247  fouriersw  46268  ovnval2  46582  hoidmvval  46614  lambert0  46917  tannpoly  46920  sinnpoly  46921  fun2dmnopgexmpl  47314  el1fzopredsuc  47355  cycl3grtrilem  47976  stgrusgra  47989  stgr1  47991  stgrnbgr0  47994  isubgr3stgrlem3  47998  isubgr3stgrlem7  48002  usgrexmpl1lem  48051  usgrexmpl1tri  48055  usgrexmpl2lem  48056  usgrexmpl2nb0  48061  usgrexmpl2nb1  48062  usgrexmpl2nb2  48063  usgrexmpl2nb3  48064  usgrexmpl2nb4  48065  usgrexmpl2nb5  48066  usgrexmpl2trifr  48067  gpgiedgdmellem  48076  gpgvtx0  48083  opgpgvtx  48085  gpgedgvtx0  48091  gpgvtxedg0  48093  gpgvtxedg1  48094  gpgedgiov  48095  gpgedg2ov  48096  gpg5nbgrvtx03starlem1  48098  gpg5nbgrvtx03starlem2  48099  gpg5nbgrvtx03starlem3  48100  gpg5nbgrvtx13starlem1  48101  gpg5nbgrvtx13starlem3  48103  gpg3nbgrvtx0  48106  gpg3nbgrvtx0ALT  48107  gpg3nbgrvtx1  48108  gpgcubic  48109  gpg5nbgr3star  48111  gpg3kgrtriex  48119  gpgprismgr4cycllem2  48126  gpgprismgr4cycllem3  48127  gpgprismgr4cycllem7  48131  gpgprismgr4cycllem9  48133  pgnioedg1  48138  pgnioedg2  48139  pgnioedg3  48140  pgnioedg4  48141  pgnioedg5  48142  pgnbgreunbgrlem1  48143  pgnbgreunbgrlem2lem1  48144  pgnbgreunbgrlem2lem2  48145  pgnbgreunbgrlem2lem3  48146  pgnbgreunbgrlem3  48148  pgnbgreunbgrlem5lem3  48152  pgnbgreunbgrlem5  48153  pgnbgreunbgrlem6  48154  gpg5edgnedg  48160  nn0mnd  48209  zlmodzxzel  48385  zlmodzxz0  48386  zlmodzxzscm  48387  zlmodzxzadd  48388  zlmodzxznm  48528  zlmodzxzldeplem  48529  zlmodzxzldeplem2  48532  blen0  48603  nn0sumshdiglemB  48651  fv1arycl  48668  1arympt1  48669  1arympt1fv  48670  1arymaptf1  48673  1arymaptfo  48674  fv2arycl  48679  2arympt  48680  2arymptfv  48681  2arymaptf1  48684  2arymaptfo  48685  ehl2eudisval0  48756  2sphere0  48781  line2ylem  48782  line2  48783  line2x  48785  line2y  48786  ex-gt  49759  ex-gte  49760  aacllem  49832