Theorem 1ex 7970

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 7922	. 2 |- 1 e. CC
2	1	elexi 2764	1 |- 1 e. _V

Syntax hints:   e. wcel 2160   _Vcvv 2752   CCcc 7827   1c1 7830

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-ext 2171  ax-1cn 7922

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-v 2754

This theorem is referenced by:  nn1suc  8956  nn0ind-raph  9388  fzprval  10100  fztpval  10101  m1expcl2  10560  1exp  10567  facnn  10725  fac0  10726  prhash2ex  10807  prodf1f  11569  fprodntrivap  11610  prod1dc  11612  fprodssdc  11616  ege2le3  11697  1nprm  12132  pcmpt  12359  dvexp  14559  dvef  14572  lgsdir2lem3  14815  2o01f  15131  iswomni0  15184