Theorem c0ex 11136

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

Syntax hints:   ∈ wcel 2119  Vcvv 3432  ℂcc 11034  0cc0 11036

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 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-mulcl 11098  ax-i2m1 11104

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434

This theorem is referenced by:  ofsubeq0  12154  ofsubge0  12156  elnn0  12437  un0mulcl  12469  fcdmnn0supp  12492  fcdmnn0fsupp  12493  fcdmnn0suppg  12494  fcdmnn0fsuppg  12495  nn0ssz  12545  nn0ind-raph  12627  xaddval  13173  xmulval  13175  ser0f  14015  facnn  14235  fac0  14236  bcval  14264  prhash2ex  14359  wrdexb  14485  s1rn  14560  eqs1  14573  repsw1  14743  cshw1  14782  s1co  14793  funcnvs2  14873  funcnvs3  14874  funcnvs4  14875  wrdlen2i  14902  wrd2pr2op  14903  wrd3tpop  14908  wwlktovf1  14917  wrdl3s3  14922  sgnval  15048  iserge0  15621  sum0  15681  sumz  15682  fsumss  15685  fsumser  15690  isumless  15808  geomulcvg  15839  rpnnen2lem1  16179  ruclem4  16199  ruclem8  16202  ruclem11  16205  0bits  16406  gcdval  16463  lcmval  16559  lcmfpr  16594  lcmfunsnlem2  16607  prmreclem2  16886  prmreclem5  16889  vdwapun  16943  smndex1n0mnd  18881  mgmnsgrpex  18900  odval  19507  odf  19510  gexval  19551  telgsumfz0  19965  telgsum  19967  srgbinom  20210  abvtrivd  20811  pzriprnglem4  21466  pzriprnglem5  21467  pzriprnglem7  21469  pzriprnglem9  21471  pzriprnglem10  21472  snifpsrbag  21902  psrbaglesupp  21904  psrbaglefi  21908  mplcoe5  22023  mplbas2  22025  ltbwe  22027  psrbag0  22045  psrbagev1  22060  mhpmulcl  22144  psdmplcl  22157  psdmvr  22164  cply1coe0bi  22295  m2cpminvid2lem  22744  pmatcollpw3fi1lem1  22776  pmatcollpw3fi1lem2  22777  pmatcollpw3fi1  22778  idpm2idmp  22791  prdsdsf  24357  prdsxmetlem  24358  prdsmet  24360  imasdsf1olem  24363  prdsbl  24481  xrge0gsumle  24824  xrge0tsms  24825  xrhmeo  24938  pcopt  25014  pcopt2  25015  pcoass  25016  rrxcph  25384  rrx0el  25390  rrxbasefi  25402  ovoliunnul  25499  ovolicc1  25508  vitalilem5  25604  mbfpos  25643  0pval  25663  0pledm  25665  i1f1lem  25681  i1f1  25682  itg11  25683  itg1addlem3  25690  itg1addlem4  25691  i1fres  25697  itg1climres  25706  mbfi1fseqlem4  25710  mbfi1fseqlem6  25712  mbfi1flimlem  25714  mbfi1flim  25715  xrge0f  25723  itg2ge0  25727  itg2uba  25735  itg2splitlem  25740  itg2monolem1  25742  itg2gt0  25752  itg2cnlem1  25753  ibl0  25779  iblcnlem1  25780  i1fibl  25800  itgeqa  25806  itgcn  25837  dvcmul  25936  dvcmulf  25937  dvexp3  25970  dvef  25972  rolle  25982  dveq0  25992  dv11cn  25993  tdeglem4  26050  elply2  26186  elplyd  26192  ply1term  26194  ply0  26198  plyeq0  26201  plypf1  26202  plymullem  26206  dgrlt  26256  plymul0or  26272  dvply1  26275  plydivlem4  26287  elqaalem2  26311  iaa  26316  aareccl  26317  aannenlem2  26320  tayl0  26352  taylpfval  26355  dvtaylp  26360  pserdvlem2  26418  abelthlem9  26430  logtayl  26649  cxplogb  26775  leibpilem2  26930  leibpi  26931  jensenlem2  26976  jensen  26977  amgmlem  26978  amgm  26979  igamval  27035  vmaval  27101  vmaf  27107  muval  27120  dchrelbas2  27225  dchrinvcl  27241  dchrptlem2  27253  lgseisenlem4  27366  addsqnreup  27431  pntrlog2bndlem4  27568  pntrlog2bndlem5  27569  padicval  27605  padicabv  27618  ostth1  27621  axlowdimlem8  29043  axlowdimlem9  29044  axlowdimlem10  29045  axlowdimlem11  29046  axlowdimlem12  29047  axlowdimlem13  29048  axlowdimlem17  29052  uspgr1ewop  29342  usgr2v1e2w  29346  umgr2v2eedg  29618  umgr2v2e  29619  umgr2v2evd2  29621  wlkl1loop  29731  2wlklem  29759  usgr2trlncl  29853  2wlkdlem4  30021  2wlkdlem5  30022  2pthdlem1  30023  2wlkdlem10  30028  usgrwwlks2on  30051  umgrwwlks2on  30052  rusgrnumwwlkl1  30064  clwwlkn2  30139  0spth  30221  1wlkdlem4  30235  wlk2v2elem1  30250  3wlkdlem4  30257  3wlkdlem5  30258  3pthdlem1  30259  3wlkdlem10  30264  upgr3v3e3cycl  30275  upgr4cycl4dv4e  30280  eulerpathpr  30335  konigsberglem4  30350  konigsberglem5  30351  wlkl0  30462  occllem  31399  0cnfn  32076  0lnfn  32081  nmfn0  32083  nmcexi  32122  nlelchi  32157  fprodex01  32924  sgncl  32930  indsupp  32953  indfsd  32954  indfsid  32955  s2rnOLD  33030  s3rnOLD  33032  gsummulsubdishift1  33156  gsummulsubdishift2s  33159  xrge0tsmsd  33161  cyc2fv1  33209  cyc3fv1  33225  cyc3evpm  33238  sgnsval  33249  sgnsf  33250  elrgspnlem1  33330  elrgspnlem4  33333  gsumind  33435  0mplrim  33705  selvply1rhmlema  33709  selvply1rhmlemb  33710  selvply1rhmlem1  33711  selvply1rhmlem2  33712  selvply1rhmlem4  33714  selvply1rhm0  33717  extvfvvcl  33726  extvfvcl  33727  esplyfval0  33755  esplysply  33762  esplyind  33766  vieta  33771  constr01  33933  constrss  33934  constrconj  33936  constrextdg2lem  33939  nn0constr  33952  xrge0iif1  34129  xrge0mulc1cn  34132  gsumesum  34250  esumpfinval  34266  esumpfinvalf  34267  ddeval1  34425  ddeval0  34426  ddemeas  34427  eulerpartlemt  34562  coinfliprv  34674  plymul02  34737  plymulx  34739  signsw0glem  34744  signsw0g  34747  signswmnd  34748  signswrid  34749  prodfzo03  34794  circlevma  34833  circlemethhgt  34834  hgt750lemg  34845  hgt750lemb  34847  hgt750lema  34848  hgt750leme  34849  tgoldbachgtde  34851  tgoldbachgt  34854  cvmliftlem4  35523  cvmliftlem5  35524  poimirlem1  37995  poimirlem2  37996  poimirlem3  37997  poimirlem4  37998  poimirlem5  37999  poimirlem6  38000  poimirlem7  38001  poimirlem11  38005  poimirlem12  38006  poimirlem16  38010  poimirlem17  38011  poimirlem19  38013  poimirlem20  38014  poimirlem22  38016  poimirlem23  38017  poimirlem24  38018  poimirlem25  38019  poimirlem28  38022  poimirlem29  38023  poimirlem31  38025  poimirlem32  38026  poimir  38027  broucube  38028  mblfinlem2  38032  mblfinlem3  38033  ismblfin  38035  itg2addnclem  38045  itg2addnclem3  38047  itg2addnc  38048  ftc1anclem3  38069  ftc1anclem5  38071  ftc1anclem7  38073  ftc1anclem8  38074  ftc1anc  38075  dvacos  38079  prdsbnd  38167  heiborlem10  38194  renegclALT  39462  aks4d1p1p4  42563  aks6d1c7lem1  42672  0prjspnlem  43080  0prjspnrel  43084  diophrw  43215  monotoddzzfi  43394  zindbi  43398  mncn0  43591  aaitgo  43614  flcidc  43622  dfrcl4  44127  fvrcllb0d  44144  fvrcllb0da  44145  iunrelexp0  44153  corclrcl  44158  relexp0idm  44166  dfrtrcl4  44189  corcltrcl  44190  cotrclrcl  44193  ofsubid  44775  lhe4.4ex1a  44780  dvsconst  44781  dvconstbi  44785  binomcxplemnn0  44800  binomcxplemdvbinom  44804  binomcxplemnotnn0  44807  n0p  45500  climrec  46055  limsup10exlem  46222  dvnmptdivc  46388  dvnmul  46393  stoweidlem55  46505  fourierdlem62  46618  fourierdlem104  46660  fouriersw  46681  ovnval2  46995  hoidmvval  47027  lambert0  47357  tannpoly  47360  sinnpoly  47361  fun2dmnopgexmpl  47754  el1fzopredsuc  47796  cycl3grtrilem  48444  stgrusgra  48457  stgr1  48459  stgrnbgr0  48462  isubgr3stgrlem3  48466  isubgr3stgrlem7  48470  usgrexmpl1lem  48519  usgrexmpl1tri  48523  usgrexmpl2lem  48524  usgrexmpl2nb0  48529  usgrexmpl2nb1  48530  usgrexmpl2nb2  48531  usgrexmpl2nb3  48532  usgrexmpl2nb4  48533  usgrexmpl2nb5  48534  usgrexmpl2trifr  48535  gpgiedgdmellem  48544  gpgvtx0  48551  opgpgvtx  48553  gpgedgvtx0  48559  gpgvtxedg0  48561  gpgvtxedg1  48562  gpgedgiov  48563  gpgedg2ov  48564  gpg5nbgrvtx03starlem1  48566  gpg5nbgrvtx03starlem2  48567  gpg5nbgrvtx03starlem3  48568  gpg5nbgrvtx13starlem1  48569  gpg5nbgrvtx13starlem3  48571  gpg3nbgrvtx0  48574  gpg3nbgrvtx0ALT  48575  gpg3nbgrvtx1  48576  gpgcubic  48577  gpg5nbgr3star  48579  gpg3kgrtriex  48587  gpgprismgr4cycllem2  48594  gpgprismgr4cycllem3  48595  gpgprismgr4cycllem7  48599  gpgprismgr4cycllem9  48601  pgnioedg1  48606  pgnioedg2  48607  pgnioedg3  48608  pgnioedg4  48609  pgnioedg5  48610  pgnbgreunbgrlem1  48611  pgnbgreunbgrlem2lem1  48612  pgnbgreunbgrlem2lem2  48613  pgnbgreunbgrlem2lem3  48614  pgnbgreunbgrlem3  48616  pgnbgreunbgrlem5lem3  48620  pgnbgreunbgrlem5  48621  pgnbgreunbgrlem6  48622  gpg5edgnedg  48628  nn0mnd  48677  zlmodzxzel  48853  zlmodzxz0  48854  zlmodzxzscm  48855  zlmodzxzadd  48856  zlmodzxznm  48995  zlmodzxzldeplem  48996  zlmodzxzldeplem2  48999  blen0  49070  nn0sumshdiglemB  49118  fv1arycl  49135  1arympt1  49136  1arympt1fv  49137  1arymaptf1  49140  1arymaptfo  49141  fv2arycl  49146  2arympt  49147  2arymptfv  49148  2arymaptf1  49151  2arymaptfo  49152  ehl2eudisval0  49223  2sphere0  49248  line2ylem  49249  line2  49250  line2x  49252  line2y  49253  ex-gt  50225  ex-gte  50226  aacllem  50298