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

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
StepHypRef Expression
1 ax-1cn 7825 . 2  |-  1  e.  CC
21elexi 2724 1  |-  1  e.  _V
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator