Theorem c0ex 8327

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

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

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 8279  ax-icn 8281  ax-addcl 8282  ax-mulcl 8284  ax-i2m1 8291

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:  ofsubeq0  9301  elnn0  9577  nn0ex  9581  un0mulcl  9609  fcdmnn0supp  9627  fcdmnn0fsupp  9628  fcdmnn0suppg  9629  fcdmnn0fsuppg  9630  nn0ssz  9674  nn0ind-raph  9775  ser0f  10993  fser0const  10994  facnn  11188  fac0  11189  prhash2ex  11273  wrdexb  11339  s1rn  11409  eqs1  11419  iserge0  12135  sum0  12181  isumz  12182  fisumss  12185  0bits  12752  bezoutlemmain  12801  lcmval  12867  psrlidmfi  15204  mvrf1fi  15215  dvef  15965  plyval  15970  elply2  15973  plyss  15976  elplyd  15979  ply1term  15981  plymullem  15988  plyco  15997  plycj  15999  uspgr1ewopdc  16702  usgr2v1e2w  16704  wlkl1loop  16816  2wlklem  16834  clwwlkn2  16879  eulerpathprum  16938  konigsberglem4  16949  konigsberglem5  16950  2o01f  17241  iswomni0  17320