Theorem c0ex 8039

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

Syntax hints:   ∈ wcel 2167  Vcvv 2763  ℂcc 7896  0cc0 7898

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-ext 2178  ax-1cn 7991  ax-icn 7993  ax-addcl 7994  ax-mulcl 7996  ax-i2m1 8003

This theorem depends on definitions:  df-bi 117  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-v 2765

This theorem is referenced by:  elnn0  9270  nn0ex  9274  un0mulcl  9302  nn0ssz  9363  nn0ind-raph  9462  ser0f  10645  fser0const  10646  facnn  10838  fac0  10839  prhash2ex  10920  wrdexb  10966  iserge0  11527  sum0  11572  isumz  11573  fisumss  11576  0bits  12143  bezoutlemmain  12192  lcmval  12258  dvef  15071  plyval  15076  elply2  15079  plyss  15082  elplyd  15085  ply1term  15087  plymullem  15094  plyco  15103  plycj  15105  2o01f  15749  iswomni0  15808