Theorem 1ex 7873

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 7825	. 2 |- 1 e. CC
2	1	elexi 2724	1 |- 1 e. _V

Syntax hints:   e. wcel 2128   _Vcvv 2712   CCcc 7730   1c1 7733

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-ext 2139  ax-1cn 7825

This theorem depends on definitions:  df-bi 116  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-v 2714

This theorem is referenced by:  nn1suc  8852  nn0ind-raph  9281  fzprval  9984  fztpval  9985  m1expcl2  10441  1exp  10448  facnn  10601  fac0  10602  prhash2ex  10683  prodf1f  11440  fprodntrivap  11481  prod1dc  11483  fprodssdc  11487  ege2le3  11568  1nprm  11991  dvexp  13086  dvef  13099  2o01f  13579  iswomni0  13633