Theorem c0ex 8273

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

Syntax hints:   ∈ wcel 2205  Vcvv 2815  ℂcc 8130  0cc0 8132

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-ext 2216  ax-1cn 8225  ax-icn 8227  ax-addcl 8228  ax-mulcl 8230  ax-i2m1 8237

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-v 2817

This theorem is referenced by:  elnn0  9503  nn0ex  9507  un0mulcl  9535  fcdmnn0supp  9553  fcdmnn0fsupp  9554  fcdmnn0suppg  9555  fcdmnn0fsuppg  9556  nn0ssz  9600  nn0ind-raph  9701  ser0f  10903  fser0const  10904  facnn  11097  fac0  11098  prhash2ex  11182  wrdexb  11244  s1rn  11314  eqs1  11324  iserge0  12036  sum0  12082  isumz  12083  fisumss  12086  0bits  12653  bezoutlemmain  12702  lcmval  12768  dvef  15641  plyval  15646  elply2  15649  plyss  15652  elplyd  15655  ply1term  15657  plymullem  15664  plyco  15673  plycj  15675  uspgr1ewopdc  16288  usgr2v1e2w  16290  wlkl1loop  16402  2wlklem  16420  clwwlkn2  16465  eulerpathprum  16524  konigsberglem4  16535  konigsberglem5  16536  2o01f  16817  iswomni0  16885