Theorem c0ex 8268

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

Syntax hints:   e. wcel 2203   _Vcvv 2813   CCcc 8125   0cc0 8127

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-ext 2214  ax-1cn 8220  ax-icn 8222  ax-addcl 8223  ax-mulcl 8225  ax-i2m1 8232

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-v 2815

This theorem is referenced by:  elnn0  9498  nn0ex  9502  un0mulcl  9530  fcdmnn0supp  9548  fcdmnn0fsupp  9549  fcdmnn0suppg  9550  fcdmnn0fsuppg  9551  nn0ssz  9595  nn0ind-raph  9695  ser0f  10896  fser0const  10897  facnn  11089  fac0  11090  prhash2ex  11174  wrdexb  11236  s1rn  11306  eqs1  11316  iserge0  12028  sum0  12074  isumz  12075  fisumss  12078  0bits  12645  bezoutlemmain  12694  lcmval  12760  dvef  15592  plyval  15597  elply2  15600  plyss  15603  elplyd  15606  ply1term  15608  plymullem  15615  plyco  15624  plycj  15626  uspgr1ewopdc  16239  usgr2v1e2w  16241  wlkl1loop  16353  2wlklem  16371  clwwlkn2  16416  eulerpathprum  16475  konigsberglem4  16486  konigsberglem5  16487  2o01f  16768  iswomni0  16836