Theorem c0ex 8066

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

Syntax hints:   e. wcel 2176   _Vcvv 2772   CCcc 7923   0cc0 7925

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-ext 2187  ax-1cn 8018  ax-icn 8020  ax-addcl 8021  ax-mulcl 8023  ax-i2m1 8030

This theorem depends on definitions:  df-bi 117  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-v 2774

This theorem is referenced by:  elnn0  9297  nn0ex  9301  un0mulcl  9329  nn0ssz  9390  nn0ind-raph  9490  ser0f  10679  fser0const  10680  facnn  10872  fac0  10873  prhash2ex  10954  wrdexb  11006  s1rn  11072  eqs1  11082  iserge0  11654  sum0  11699  isumz  11700  fisumss  11703  0bits  12270  bezoutlemmain  12319  lcmval  12385  dvef  15199  plyval  15204  elply2  15207  plyss  15210  elplyd  15213  ply1term  15215  plymullem  15222  plyco  15231  plycj  15233  2o01f  15931  iswomni0  15990