Theorem c0ex 8073

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

Syntax hints:   ∈ wcel 2177  Vcvv 2773  ℂcc 7930  0cc0 7932

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-ext 2188  ax-1cn 8025  ax-icn 8027  ax-addcl 8028  ax-mulcl 8030  ax-i2m1 8037

This theorem depends on definitions:  df-bi 117  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-v 2775

This theorem is referenced by:  elnn0  9304  nn0ex  9308  un0mulcl  9336  nn0ssz  9397  nn0ind-raph  9497  ser0f  10686  fser0const  10687  facnn  10879  fac0  10880  prhash2ex  10961  wrdexb  11013  s1rn  11080  eqs1  11090  iserge0  11698  sum0  11743  isumz  11744  fisumss  11747  0bits  12314  bezoutlemmain  12363  lcmval  12429  dvef  15243  plyval  15248  elply2  15251  plyss  15254  elplyd  15257  ply1term  15259  plymullem  15266  plyco  15275  plycj  15277  2o01f  16005  iswomni0  16064