Theorem c0ex 8178

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

Syntax hints:   ∈ wcel 2201  Vcvv 2801  ℂcc 8035  0cc0 8037

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-ext 2212  ax-1cn 8130  ax-icn 8132  ax-addcl 8133  ax-mulcl 8135  ax-i2m1 8142

This theorem depends on definitions:  df-bi 117  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-v 2803

This theorem is referenced by:  elnn0  9409  nn0ex  9413  un0mulcl  9441  nn0ssz  9502  nn0ind-raph  9602  ser0f  10802  fser0const  10803  facnn  10995  fac0  10996  prhash2ex  11079  wrdexb  11134  s1rn  11204  eqs1  11214  iserge0  11926  sum0  11972  isumz  11973  fisumss  11976  0bits  12543  bezoutlemmain  12592  lcmval  12658  dvef  15480  plyval  15485  elply2  15488  plyss  15491  elplyd  15494  ply1term  15496  plymullem  15503  plyco  15512  plycj  15514  uspgr1ewopdc  16124  usgr2v1e2w  16126  wlkl1loop  16238  2wlklem  16256  clwwlkn2  16301  eulerpathprum  16360  konigsberglem4  16371  konigsberglem5  16372  2o01f  16653  iswomni0  16723