Theorem c0ex 8216

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

Syntax hints:   e. wcel 2202   _Vcvv 2803   CCcc 8073   0cc0 8075

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 2213  ax-1cn 8168  ax-icn 8170  ax-addcl 8171  ax-mulcl 8173  ax-i2m1 8180

This theorem depends on definitions:  df-bi 117  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-v 2805

This theorem is referenced by:  elnn0  9446  nn0ex  9450  un0mulcl  9478  fcdmnn0supp  9496  fcdmnn0suppg  9497  nn0ssz  9541  nn0ind-raph  9641  ser0f  10842  fser0const  10843  facnn  11035  fac0  11036  prhash2ex  11119  wrdexb  11174  s1rn  11244  eqs1  11254  iserge0  11966  sum0  12012  isumz  12013  fisumss  12016  0bits  12583  bezoutlemmain  12632  lcmval  12698  dvef  15521  plyval  15526  elply2  15529  plyss  15532  elplyd  15535  ply1term  15537  plymullem  15544  plyco  15553  plycj  15555  uspgr1ewopdc  16168  usgr2v1e2w  16170  wlkl1loop  16282  2wlklem  16300  clwwlkn2  16345  eulerpathprum  16404  konigsberglem4  16415  konigsberglem5  16416  2o01f  16697  iswomni0  16767