Theorem c0ex 8163

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

Syntax hints:   e. wcel 2200   _Vcvv 2800   CCcc 8020   0cc0 8022

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-ext 2211  ax-1cn 8115  ax-icn 8117  ax-addcl 8118  ax-mulcl 8120  ax-i2m1 8127

This theorem depends on definitions:  df-bi 117  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-v 2802

This theorem is referenced by:  elnn0  9394  nn0ex  9398  un0mulcl  9426  nn0ssz  9487  nn0ind-raph  9587  ser0f  10786  fser0const  10787  facnn  10979  fac0  10980  prhash2ex  11063  wrdexb  11115  s1rn  11185  eqs1  11195  iserge0  11894  sum0  11939  isumz  11940  fisumss  11943  0bits  12510  bezoutlemmain  12559  lcmval  12625  dvef  15441  plyval  15446  elply2  15449  plyss  15452  elplyd  15455  ply1term  15457  plymullem  15464  plyco  15473  plycj  15475  uspgr1ewopdc  16083  usgr2v1e2w  16085  wlkl1loop  16155  2wlklem  16171  clwwlkn2  16216  2o01f  16529  iswomni0  16591