Theorem c0ex 7632

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

Syntax hints:   ∈ wcel 1448  Vcvv 2641  ℂcc 7498  0cc0 7500

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-ext 2082  ax-1cn 7588  ax-icn 7590  ax-addcl 7591  ax-mulcl 7593  ax-i2m1 7600

This theorem depends on definitions:  df-bi 116  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-v 2643

This theorem is referenced by:  elnn0  8831  nn0ex  8835  un0mulcl  8863  nn0ssz  8924  nn0ind-raph  9020  ser0f  10129  fser0const  10130  facnn  10314  fac0  10315  prhash2ex  10396  iserge0  10951  sum0  10996  isumz  10997  fisumss  11000  bezoutlemmain  11479  lcmval  11537  isomninnlem  12809