Theorem 1ex 8016

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 7967	. 2 |- 1 e. CC
2	1	elexi 2772	1 |- 1 e. _V

Syntax hints:   e. wcel 2164   _Vcvv 2760   CCcc 7872   1c1 7875

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 2175  ax-1cn 7967

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-v 2762

This theorem is referenced by:  nn1suc  9003  nn0ind-raph  9437  fzprval  10151  fztpval  10152  m1expcl2  10635  1exp  10642  facnn  10801  fac0  10802  prhash2ex  10883  prodf1f  11689  fprodntrivap  11730  prod1dc  11732  fprodssdc  11736  ege2le3  11817  1nprm  12255  pcmpt  12484  dvexp  14890  dvef  14906  lgsdir2lem3  15187  2o01f  15557  iswomni0  15611