Theorem c0ex 8320

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

This proof depends on syntax axioms:   ∈ wcel 2209  Vcvv 2821  ℂcc 8177  0cc0 8179

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-ext 2220  ax-1cn 8272  ax-icn 8274  ax-addcl 8275  ax-mulcl 8277  ax-i2m1 8284

This proof depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is used by:  elnn0  9567  nn0ex  9571  un0mulcl  9599  fcdmnn0supp  9617  fcdmnn0fsupp  9618  fcdmnn0suppg  9619  fcdmnn0fsuppg  9620  nn0ssz  9664  nn0ind-raph  9765  ser0f  10973  fser0const  10974  facnn  11167  fac0  11168  prhash2ex  11252  wrdexb  11318  s1rn  11388  eqs1  11398  iserge0  12111  sum0  12157  isumz  12158  fisumss  12161  0bits  12728  bezoutlemmain  12777  lcmval  12843  dvef  15830  plyval  15835  elply2  15838  plyss  15841  elplyd  15844  ply1term  15846  plymullem  15853  plyco  15862  plycj  15864  uspgr1ewopdc  16497  usgr2v1e2w  16499  wlkl1loop  16611  2wlklem  16629  clwwlkn2  16674  eulerpathprum  16733  konigsberglem4  16744  konigsberglem5  16745  2o01f  17036  iswomni0  17113