ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  1ex Unicode version

Theorem 1ex 7951
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
StepHypRef Expression
1 ax-1cn 7903 . 2  |-  1  e.  CC
21elexi 2749 1  |-  1  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 2148   _Vcvv 2737   CCcc 7808   1c1 7811
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 7903
This theorem depends on definitions:  df-bi 117  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-v 2739
This theorem is referenced by:  nn1suc  8937  nn0ind-raph  9369  fzprval  10081  fztpval  10082  m1expcl2  10541  1exp  10548  facnn  10706  fac0  10707  prhash2ex  10788  prodf1f  11550  fprodntrivap  11591  prod1dc  11593  fprodssdc  11597  ege2le3  11678  1nprm  12113  pcmpt  12340  dvexp  14145  dvef  14158  lgsdir2lem3  14401  2o01f  14716  iswomni0  14769
  Copyright terms: Public domain W3C validator