Theorem c0ex 8173

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

Syntax hints:   ∈ wcel 2202  Vcvv 2802  ℂcc 8030  0cc0 8032

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-ext 2213  ax-1cn 8125  ax-icn 8127  ax-addcl 8128  ax-mulcl 8130  ax-i2m1 8137

This theorem depends on definitions:  df-bi 117  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-v 2804

This theorem is referenced by:  elnn0  9404  nn0ex  9408  un0mulcl  9436  nn0ssz  9497  nn0ind-raph  9597  ser0f  10797  fser0const  10798  facnn  10990  fac0  10991  prhash2ex  11074  wrdexb  11126  s1rn  11196  eqs1  11206  iserge0  11905  sum0  11951  isumz  11952  fisumss  11955  0bits  12522  bezoutlemmain  12571  lcmval  12637  dvef  15454  plyval  15459  elply2  15462  plyss  15465  elplyd  15468  ply1term  15470  plymullem  15477  plyco  15486  plycj  15488  uspgr1ewopdc  16098  usgr2v1e2w  16100  wlkl1loop  16212  2wlklem  16230  clwwlkn2  16275  2o01f  16614  iswomni0  16676