Theorem c0ex 8156

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

Syntax hints:   ∈ wcel 2200  Vcvv 2799  ℂcc 8013  0cc0 8015

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-ext 2211  ax-1cn 8108  ax-icn 8110  ax-addcl 8111  ax-mulcl 8113  ax-i2m1 8120

This theorem depends on definitions:  df-bi 117  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-v 2801

This theorem is referenced by:  elnn0  9387  nn0ex  9391  un0mulcl  9419  nn0ssz  9480  nn0ind-raph  9580  ser0f  10773  fser0const  10774  facnn  10966  fac0  10967  prhash2ex  11049  wrdexb  11101  s1rn  11171  eqs1  11181  iserge0  11875  sum0  11920  isumz  11921  fisumss  11924  0bits  12491  bezoutlemmain  12540  lcmval  12606  dvef  15422  plyval  15427  elply2  15430  plyss  15433  elplyd  15436  ply1term  15438  plymullem  15445  plyco  15454  plycj  15456  uspgr1ewopdc  16063  usgr2v1e2w  16065  wlkl1loop  16130  2wlklem  16146  clwwlkn2  16189  2o01f  16471  iswomni0  16533