Theorem 1ex 7952

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 7904	. 2 |- 1 e. CC
2	1	elexi 2750	1 |- 1 e. _V

Syntax hints:   e. wcel 2148   _Vcvv 2738   CCcc 7809   1c1 7812

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-ext 2159  ax-1cn 7904

This theorem depends on definitions:  df-bi 117  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-v 2740

This theorem is referenced by:  nn1suc  8938  nn0ind-raph  9370  fzprval  10082  fztpval  10083  m1expcl2  10542  1exp  10549  facnn  10707  fac0  10708  prhash2ex  10789  prodf1f  11551  fprodntrivap  11592  prod1dc  11594  fprodssdc  11598  ege2le3  11679  1nprm  12114  pcmpt  12341  dvexp  14178  dvef  14191  lgsdir2lem3  14434  2o01f  14749  iswomni0  14802