Theorem c0ex 8310

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

Syntax hints:   e. wcel 2209   _Vcvv 2821   CCcc 8167   0cc0 8169

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 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 8262  ax-icn 8264  ax-addcl 8265  ax-mulcl 8267  ax-i2m1 8274

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

This theorem is referenced by:  elnn0  9544  nn0ex  9548  un0mulcl  9576  fcdmnn0supp  9594  fcdmnn0fsupp  9595  fcdmnn0suppg  9596  fcdmnn0fsuppg  9597  nn0ssz  9641  nn0ind-raph  9742  ser0f  10949  fser0const  10950  facnn  11143  fac0  11144  prhash2ex  11228  wrdexb  11294  s1rn  11364  eqs1  11374  iserge0  12087  sum0  12133  isumz  12134  fisumss  12137  0bits  12704  bezoutlemmain  12753  lcmval  12819  dvef  15751  plyval  15756  elply2  15759  plyss  15762  elplyd  15765  ply1term  15767  plymullem  15774  plyco  15783  plycj  15785  uspgr1ewopdc  16399  usgr2v1e2w  16401  wlkl1loop  16513  2wlklem  16531  clwwlkn2  16576  eulerpathprum  16635  konigsberglem4  16646  konigsberglem5  16647  2o01f  16938  iswomni0  17006