Theorem c0ex 8320

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

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

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 8272  ax-icn 8274  ax-addcl 8275  ax-mulcl 8277  ax-i2m1 8284

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:  elnn0  9569  nn0ex  9573  un0mulcl  9601  fcdmnn0supp  9619  fcdmnn0fsupp  9620  fcdmnn0suppg  9621  fcdmnn0fsuppg  9622  nn0ssz  9666  nn0ind-raph  9767  ser0f  10984  fser0const  10985  facnn  11179  fac0  11180  prhash2ex  11264  wrdexb  11330  s1rn  11400  eqs1  11410  iserge0  12125  sum0  12171  isumz  12172  fisumss  12175  0bits  12742  bezoutlemmain  12791  lcmval  12857  dvef  15877  plyval  15882  elply2  15885  plyss  15888  elplyd  15891  ply1term  15893  plymullem  15900  plyco  15909  plycj  15911  uspgr1ewopdc  16583  usgr2v1e2w  16585  wlkl1loop  16697  2wlklem  16715  clwwlkn2  16760  eulerpathprum  16819  konigsberglem4  16830  konigsberglem5  16831  2o01f  17122  iswomni0  17199