Theorem c0ex 8326

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

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

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 8278  ax-icn 8280  ax-addcl 8281  ax-mulcl 8283  ax-i2m1 8290

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:  ofsubeq0  9300  elnn0  9576  nn0ex  9580  un0mulcl  9608  fcdmnn0supp  9626  fcdmnn0suppg  9627  nn0ssz  9671  nn0ind-raph  9773  ser0f  10991  fser0const  10992  facnn  11186  fac0  11187  prhash2ex  11271  wrdexb  11337  s1rn  11407  eqs1  11417  iserge0  12133  sum0  12179  isumz  12180  fisumss  12183  0bits  12750  bezoutlemmain  12799  lcmval  12865  psrlidmfi  15208  mvrf1fi  15219  dvef  15970  plyval  15975  elply2  15978  plyss  15981  elplyd  15984  ply1term  15986  plymullem  15993  plyco  16002  plycj  16004  uspgr1ewopdc  16707  usgr2v1e2w  16709  wlkl1loop  16821  2wlklem  16839  clwwlkn2  16884  eulerpathprum  16943  konigsberglem4  16954  konigsberglem5  16955  2o01f  17246  iswomni0  17325