Theorem c0ex 8173

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 8171	. 2 |- 0 e. CC
2	1	elexi 2815	1 |- 0 e. _V

Syntax hints:   e. wcel 2202   _Vcvv 2802   CCcc 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  11129  s1rn  11199  eqs1  11209  iserge0  11921  sum0  11967  isumz  11968  fisumss  11971  0bits  12538  bezoutlemmain  12587  lcmval  12653  dvef  15470  plyval  15475  elply2  15478  plyss  15481  elplyd  15484  ply1term  15486  plymullem  15493  plyco  15502  plycj  15504  uspgr1ewopdc  16114  usgr2v1e2w  16116  wlkl1loop  16228  2wlklem  16246  clwwlkn2  16291  eulerpathprum  16350  konigsberglem4  16361  konigsberglem5  16362  2o01f  16644  iswomni0  16707