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

Theorem 1ex 7981
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 7933 . 2 1 ∈ ℂ
21elexi 2764 1 1 ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 2160  Vcvv 2752  cc 7838  1c1 7841
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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-ext 2171  ax-1cn 7933
This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-v 2754
This theorem is referenced by:  nn1suc  8967  nn0ind-raph  9399  fzprval  10111  fztpval  10112  m1expcl2  10572  1exp  10579  facnn  10738  fac0  10739  prhash2ex  10820  prodf1f  11582  fprodntrivap  11623  prod1dc  11625  fprodssdc  11629  ege2le3  11710  1nprm  12145  pcmpt  12374  dvexp  14627  dvef  14640  lgsdir2lem3  14884  2o01f  15200  iswomni0  15253
  Copyright terms: Public domain W3C validator