Theorem c0ex 8108

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

Syntax hints:   ∈ wcel 2180  Vcvv 2779  ℂcc 7965  0cc0 7967

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 1473  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-ext 2191  ax-1cn 8060  ax-icn 8062  ax-addcl 8063  ax-mulcl 8065  ax-i2m1 8072

This theorem depends on definitions:  df-bi 117  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-v 2781

This theorem is referenced by:  elnn0  9339  nn0ex  9343  un0mulcl  9371  nn0ssz  9432  nn0ind-raph  9532  ser0f  10723  fser0const  10724  facnn  10916  fac0  10917  prhash2ex  10998  wrdexb  11050  s1rn  11117  eqs1  11127  iserge0  11820  sum0  11865  isumz  11866  fisumss  11869  0bits  12436  bezoutlemmain  12485  lcmval  12551  dvef  15366  plyval  15371  elply2  15374  plyss  15377  elplyd  15380  ply1term  15382  plymullem  15389  plyco  15398  plycj  15400  2o01f  16269  iswomni0  16330