Theorem c0ex 8020

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

Syntax hints:   e. wcel 2167   _Vcvv 2763   CCcc 7877   0cc0 7879

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 7972  ax-icn 7974  ax-addcl 7975  ax-mulcl 7977  ax-i2m1 7984

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  9251  nn0ex  9255  un0mulcl  9283  nn0ssz  9344  nn0ind-raph  9443  ser0f  10626  fser0const  10627  facnn  10819  fac0  10820  prhash2ex  10901  wrdexb  10947  iserge0  11508  sum0  11553  isumz  11554  fisumss  11557  bezoutlemmain  12165  lcmval  12231  dvef  14963  plyval  14968  elply2  14971  plyss  14974  elplyd  14977  ply1term  14979  plymullem  14986  plyco  14995  plycj  14997  2o01f  15641  iswomni0  15695