Theorem c0ex 8172

Description: 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)

Assertion

Ref	Expression
c0ex	|- 0 e. _V

Proof of Theorem c0ex

Step	Hyp	Ref	Expression
1		0cn 8170	. 2 |- 0 e. CC
2	1	elexi 2815	1 |- 0 e. _V

Syntax hints:   e. wcel 2202   _Vcvv 2802   CCcc 8029   0cc0 8031

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 8124  ax-icn 8126  ax-addcl 8127  ax-mulcl 8129  ax-i2m1 8136

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  9403  nn0ex  9407  un0mulcl  9435  nn0ssz  9496  nn0ind-raph  9596  ser0f  10795  fser0const  10796  facnn  10988  fac0  10989  prhash2ex  11072  wrdexb  11124  s1rn  11194  eqs1  11204  iserge0  11903  sum0  11948  isumz  11949  fisumss  11952  0bits  12519  bezoutlemmain  12568  lcmval  12634  dvef  15450  plyval  15455  elply2  15458  plyss  15461  elplyd  15464  ply1term  15466  plymullem  15473  plyco  15482  plycj  15484  uspgr1ewopdc  16094  usgr2v1e2w  16096  wlkl1loop  16208  2wlklem  16226  clwwlkn2  16271  2o01f  16593  iswomni0  16655