Theorem c0ex 8022

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

Syntax hints:   ∈ wcel 2167  Vcvv 2763  ℂcc 7879  0cc0 7881

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 7974  ax-icn 7976  ax-addcl 7977  ax-mulcl 7979  ax-i2m1 7986

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  9253  nn0ex  9257  un0mulcl  9285  nn0ssz  9346  nn0ind-raph  9445  ser0f  10628  fser0const  10629  facnn  10821  fac0  10822  prhash2ex  10903  wrdexb  10949  iserge0  11510  sum0  11555  isumz  11556  fisumss  11559  0bits  12126  bezoutlemmain  12175  lcmval  12241  dvef  14973  plyval  14978  elply2  14981  plyss  14984  elplyd  14987  ply1term  14989  plymullem  14996  plyco  15005  plycj  15007  2o01f  15651  iswomni0  15705