Theorem c0ex 8037

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

Syntax hints:   e. wcel 2167   _Vcvv 2763   CCcc 7894   0cc0 7896

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-ext 2178  ax-1cn 7989  ax-icn 7991  ax-addcl 7992  ax-mulcl 7994  ax-i2m1 8001

This theorem depends on definitions:  df-bi 117  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-v 2765

This theorem is referenced by:  elnn0  9268  nn0ex  9272  un0mulcl  9300  nn0ssz  9361  nn0ind-raph  9460  ser0f  10643  fser0const  10644  facnn  10836  fac0  10837  prhash2ex  10918  wrdexb  10964  iserge0  11525  sum0  11570  isumz  11571  fisumss  11574  0bits  12141  bezoutlemmain  12190  lcmval  12256  dvef  15047  plyval  15052  elply2  15055  plyss  15058  elplyd  15061  ply1term  15063  plymullem  15070  plyco  15079  plycj  15081  2o01f  15725  iswomni0  15782