Theorem c0ex 8284

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

Syntax hints:   ∈ wcel 2205  Vcvv 2815  ℂcc 8141  0cc0 8143

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 2216  ax-1cn 8236  ax-icn 8238  ax-addcl 8239  ax-mulcl 8241  ax-i2m1 8248

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-v 2817

This theorem is referenced by:  elnn0  9518  nn0ex  9522  un0mulcl  9550  fcdmnn0supp  9568  fcdmnn0fsupp  9569  fcdmnn0suppg  9570  fcdmnn0fsuppg  9571  nn0ssz  9615  nn0ind-raph  9716  ser0f  10923  fser0const  10924  facnn  11117  fac0  11118  prhash2ex  11202  wrdexb  11264  s1rn  11334  eqs1  11344  iserge0  12056  sum0  12102  isumz  12103  fisumss  12106  0bits  12673  bezoutlemmain  12722  lcmval  12788  dvef  15721  plyval  15726  elply2  15729  plyss  15732  elplyd  15735  ply1term  15737  plymullem  15744  plyco  15753  plycj  15755  uspgr1ewopdc  16368  usgr2v1e2w  16370  wlkl1loop  16482  2wlklem  16500  clwwlkn2  16545  eulerpathprum  16604  konigsberglem4  16615  konigsberglem5  16616  2o01f  16907  iswomni0  16975