Theorem c0ex 8326

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

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

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 8278  ax-icn 8280  ax-addcl 8281  ax-mulcl 8283  ax-i2m1 8290

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:  ofsubeq0  9300  elnn0  9576  nn0ex  9580  un0mulcl  9608  fcdmnn0supp  9626  fcdmnn0fsupp  9627  fcdmnn0suppg  9628  fcdmnn0fsuppg  9629  nn0ssz  9673  nn0ind-raph  9774  ser0f  10992  fser0const  10993  facnn  11187  fac0  11188  prhash2ex  11272  wrdexb  11338  s1rn  11408  eqs1  11418  iserge0  12134  sum0  12180  isumz  12181  fisumss  12184  0bits  12751  bezoutlemmain  12800  lcmval  12866  psrlidmfi  15199  dvef  15953  plyval  15958  elply2  15961  plyss  15964  elplyd  15967  ply1term  15969  plymullem  15976  plyco  15985  plycj  15987  uspgr1ewopdc  16690  usgr2v1e2w  16692  wlkl1loop  16804  2wlklem  16822  clwwlkn2  16867  eulerpathprum  16926  konigsberglem4  16937  konigsberglem5  16938  2o01f  17229  iswomni0  17308