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

Theorem 1ex 7915
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 7867 . 2  |-  1  e.  CC
21elexi 2742 1  |-  1  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 2141   _Vcvv 2730   CCcc 7772   1c1 7775
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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-ext 2152  ax-1cn 7867
This theorem depends on definitions:  df-bi 116  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-v 2732
This theorem is referenced by:  nn1suc  8897  nn0ind-raph  9329  fzprval  10038  fztpval  10039  m1expcl2  10498  1exp  10505  facnn  10661  fac0  10662  prhash2ex  10744  prodf1f  11506  fprodntrivap  11547  prod1dc  11549  fprodssdc  11553  ege2le3  11634  1nprm  12068  pcmpt  12295  dvexp  13469  dvef  13482  lgsdir2lem3  13725  2o01f  14029  iswomni0  14083
  Copyright terms: Public domain W3C validator