Theorem 1ex 8067

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

Syntax hints:   e. wcel 2176   _Vcvv 2772   CCcc 7923   1c1 7926

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 8018

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  9055  nn0ind-raph  9490  fzprval  10204  fztpval  10205  m1expcl2  10706  1exp  10713  facnn  10872  fac0  10873  prhash2ex  10954  prodf1f  11854  fprodntrivap  11895  prod1dc  11897  fprodssdc  11901  ege2le3  11982  1nprm  12436  pcmpt  12666  dvexp  15183  dvef  15199  lgsdir2lem3  15507  2o01f  15935  iswomni0  15994