Theorem c0ex 8284

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

Syntax hints:   e. wcel 2205   _Vcvv 2815   CCcc 8141   0cc0 8143

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 2216  ax-1cn 8236  ax-icn 8238  ax-addcl 8239  ax-mulcl 8241  ax-i2m1 8248

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-v 2817

This theorem is referenced by:  elnn0  9515  nn0ex  9519  un0mulcl  9547  fcdmnn0supp  9565  fcdmnn0fsupp  9566  fcdmnn0suppg  9567  fcdmnn0fsuppg  9568  nn0ssz  9612  nn0ind-raph  9713  ser0f  10920  fser0const  10921  facnn  11114  fac0  11115  prhash2ex  11199  wrdexb  11261  s1rn  11331  eqs1  11341  iserge0  12053  sum0  12099  isumz  12100  fisumss  12103  0bits  12670  bezoutlemmain  12719  lcmval  12785  dvef  15718  plyval  15723  elply2  15726  plyss  15729  elplyd  15732  ply1term  15734  plymullem  15741  plyco  15750  plycj  15752  uspgr1ewopdc  16365  usgr2v1e2w  16367  wlkl1loop  16479  2wlklem  16497  clwwlkn2  16542  eulerpathprum  16601  konigsberglem4  16612  konigsberglem5  16613  2o01f  16894  iswomni0  16962