Theorem 1ex 8174

Description: 1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.)

Assertion

Ref	Expression
1ex	|- 1 e. _V

Proof of Theorem 1ex

Step	Hyp	Ref	Expression
1		ax-1cn 8125	. 2 |- 1 e. CC
2	1	elexi 2815	1 |- 1 e. _V

Syntax hints:   e. wcel 2202   _Vcvv 2802   CCcc 8030   1c1 8033

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-ext 2213  ax-1cn 8125

This theorem depends on definitions:  df-bi 117  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-v 2804

This theorem is referenced by:  nn1suc  9162  nn0ind-raph  9597  fzprval  10317  fztpval  10318  m1expcl2  10824  1exp  10831  facnn  10990  fac0  10991  prhash2ex  11074  prodf1f  12122  fprodntrivap  12163  prod1dc  12165  fprodssdc  12169  ege2le3  12250  1nprm  12704  pcmpt  12934  dvexp  15454  dvef  15470  lgsdir2lem3  15778  2wlklem  16246  konigsberglem4  16361  konigsberglem5  16362  2o01f  16644  iswomni0  16707