Theorem c0ex 8314

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

Step	Hyp	Ref	Expression
1		0cn 8312	. 2 ⊢ 0 ∈ ℂ
2	1	elexi 2834	1 ⊢ 0 ∈ V

Syntax hints:   ∈ wcel 2209  Vcvv 2821  ℂcc 8171  0cc0 8173

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-ext 2220  ax-1cn 8266  ax-icn 8268  ax-addcl 8269  ax-mulcl 8271  ax-i2m1 8278

This theorem depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is referenced by:  elnn0  9548  nn0ex  9552  un0mulcl  9580  fcdmnn0supp  9598  fcdmnn0fsupp  9599  fcdmnn0suppg  9600  fcdmnn0fsuppg  9601  nn0ssz  9645  nn0ind-raph  9746  ser0f  10954  fser0const  10955  facnn  11148  fac0  11149  prhash2ex  11233  wrdexb  11299  s1rn  11369  eqs1  11379  iserge0  12092  sum0  12138  isumz  12139  fisumss  12142  0bits  12709  bezoutlemmain  12758  lcmval  12824  dvef  15811  plyval  15816  elply2  15819  plyss  15822  elplyd  15825  ply1term  15827  plymullem  15834  plyco  15843  plycj  15845  uspgr1ewopdc  16468  usgr2v1e2w  16470  wlkl1loop  16582  2wlklem  16600  clwwlkn2  16645  eulerpathprum  16704  konigsberglem4  16715  konigsberglem5  16716  2o01f  17007  iswomni0  17075