Theorem c0ex 8264

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

Syntax hints:   ∈ wcel 2203  Vcvv 2812  ℂcc 8121  0cc0 8123

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-ext 2214  ax-1cn 8216  ax-icn 8218  ax-addcl 8219  ax-mulcl 8221  ax-i2m1 8228

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-v 2814

This theorem is referenced by:  elnn0  9494  nn0ex  9498  un0mulcl  9526  fcdmnn0supp  9544  fcdmnn0fsupp  9545  fcdmnn0suppg  9546  fcdmnn0fsuppg  9547  nn0ssz  9591  nn0ind-raph  9691  ser0f  10892  fser0const  10893  facnn  11085  fac0  11086  prhash2ex  11169  wrdexb  11229  s1rn  11299  eqs1  11309  iserge0  12021  sum0  12067  isumz  12068  fisumss  12071  0bits  12638  bezoutlemmain  12687  lcmval  12753  dvef  15579  plyval  15584  elply2  15587  plyss  15590  elplyd  15593  ply1term  15595  plymullem  15602  plyco  15611  plycj  15613  uspgr1ewopdc  16226  usgr2v1e2w  16228  wlkl1loop  16340  2wlklem  16358  clwwlkn2  16403  eulerpathprum  16462  konigsberglem4  16473  konigsberglem5  16474  2o01f  16755  iswomni0  16823