Theorem c0ex 8321

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

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

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 8273  ax-icn 8275  ax-addcl 8276  ax-mulcl 8278  ax-i2m1 8285

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  9570  nn0ex  9574  un0mulcl  9602  fcdmnn0supp  9620  fcdmnn0fsupp  9621  fcdmnn0suppg  9622  fcdmnn0fsuppg  9623  nn0ssz  9667  nn0ind-raph  9768  ser0f  10986  fser0const  10987  facnn  11181  fac0  11182  prhash2ex  11266  wrdexb  11332  s1rn  11402  eqs1  11412  iserge0  12128  sum0  12174  isumz  12175  fisumss  12178  0bits  12745  bezoutlemmain  12794  lcmval  12860  dvef  15919  plyval  15924  elply2  15927  plyss  15930  elplyd  15933  ply1term  15935  plymullem  15942  plyco  15951  plycj  15953  uspgr1ewopdc  16656  usgr2v1e2w  16658  wlkl1loop  16770  2wlklem  16788  clwwlkn2  16833  eulerpathprum  16892  konigsberglem4  16903  konigsberglem5  16904  2o01f  17195  iswomni0  17273