Theorem 1ex 8069

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 8020	. 2 |- 1 e. CC
2	1	elexi 2784	1 |- 1 e. _V

Syntax hints:   e. wcel 2176   _Vcvv 2772   CCcc 7925   1c1 7928

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-ext 2187  ax-1cn 8020

This theorem depends on definitions:  df-bi 117  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-v 2774

This theorem is referenced by:  nn1suc  9057  nn0ind-raph  9492  fzprval  10206  fztpval  10207  m1expcl2  10708  1exp  10715  facnn  10874  fac0  10875  prhash2ex  10956  prodf1f  11887  fprodntrivap  11928  prod1dc  11930  fprodssdc  11934  ege2le3  12015  1nprm  12469  pcmpt  12699  dvexp  15216  dvef  15232  lgsdir2lem3  15540  2o01f  15968  iswomni0  16027