Theorem c0ex 8320

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

This proof depends on syntax axioms:   e. wcel 2209   _Vcvv 2821   CCcc 8177   0cc0 8179

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-ext 2220  ax-1cn 8272  ax-icn 8274  ax-addcl 8275  ax-mulcl 8277  ax-i2m1 8284

This proof depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is used by:  elnn0  9565  nn0ex  9569  un0mulcl  9597  fcdmnn0supp  9615  fcdmnn0fsupp  9616  fcdmnn0suppg  9617  fcdmnn0fsuppg  9618  nn0ssz  9662  nn0ind-raph  9763  ser0f  10971  fser0const  10972  facnn  11165  fac0  11166  prhash2ex  11250  wrdexb  11316  s1rn  11386  eqs1  11396  iserge0  12109  sum0  12155  isumz  12156  fisumss  12159  0bits  12726  bezoutlemmain  12775  lcmval  12841  dvef  15828  plyval  15833  elply2  15836  plyss  15839  elplyd  15842  ply1term  15844  plymullem  15851  plyco  15860  plycj  15862  uspgr1ewopdc  16485  usgr2v1e2w  16487  wlkl1loop  16599  2wlklem  16617  clwwlkn2  16662  eulerpathprum  16721  konigsberglem4  16732  konigsberglem5  16733  2o01f  17024  iswomni0  17101