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

Theorem 1ex 7902
Description: 1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
1ex 1 ∈ V

Proof of Theorem 1ex
StepHypRef Expression
1 ax-1cn 7854 . 2 1 ∈ ℂ
21elexi 2742 1 1 ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 2141  Vcvv 2730  cc 7759  1c1 7762
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 7854
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  8884  nn0ind-raph  9316  fzprval  10025  fztpval  10026  m1expcl2  10485  1exp  10492  facnn  10648  fac0  10649  prhash2ex  10731  prodf1f  11493  fprodntrivap  11534  prod1dc  11536  fprodssdc  11540  ege2le3  11621  1nprm  12055  pcmpt  12282  dvexp  13428  dvef  13441  lgsdir2lem3  13684  2o01f  13989  iswomni0  14043
  Copyright terms: Public domain W3C validator