Theorem c0ex 8013

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

Syntax hints:   e. wcel 2164   _Vcvv 2760   CCcc 7870   0cc0 7872

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-ext 2175  ax-1cn 7965  ax-icn 7967  ax-addcl 7968  ax-mulcl 7970  ax-i2m1 7977

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-v 2762

This theorem is referenced by:  elnn0  9242  nn0ex  9246  un0mulcl  9274  nn0ssz  9335  nn0ind-raph  9434  ser0f  10605  fser0const  10606  facnn  10798  fac0  10799  prhash2ex  10880  wrdexb  10926  iserge0  11486  sum0  11531  isumz  11532  fisumss  11535  bezoutlemmain  12135  lcmval  12201  dvef  14873  plyval  14878  elply2  14881  plyss  14884  elplyd  14887  ply1term  14889  plymullem  14896  2o01f  15487  iswomni0  15541