MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1ex Unicode version

Theorem 1ex 8833
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 8795 . 2  |-  1  e.  CC
21elexi 2797 1  |-  1  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   _Vcvv 2788   CCcc 8735   1c1 8738
This theorem is referenced by:  1nn  9757  dfnn2  9759  nn1suc  9767  nn0ind-raph  10112  fzprval  10844  fztpval  10845  expval  11106  m1expcl2  11125  1exp  11131  facnn  11290  fac0  11291  harmonic  12317  ege2le3  12371  ruclem8  12515  1nprm  12763  isprm2lem  12765  pcmpt  12940  abvtrivd  15605  imasdsf1olem  17937  pcopt  18520  pcopt2  18521  pcoass  18522  voliunlem1  18907  i1f1lem  19044  i1f1  19045  itg11  19046  iblcnlem1  19142  bddibl  19194  dvexp  19302  mvth  19339  aalioulem2  19713  efrlim  20264  basellem7  20324  basellem9  20326  ppiublem2  20442  pclogsum  20454  perfectlem2  20469  bposlem5  20527  lgsfval  20540  lgsdir2lem3  20564  lgsdir  20569  lgsdilem2  20570  lgsdi  20571  lgsne0  20572  ostth1  20782  ex-xp  20823  nmopun  22594  pjnmopi  22728  cntnevol  23175  coinfliprv  23683  subfacp1lem1  23710  subfacp1lem2a  23711  subfacp1lem3  23713  subfacp1lem5  23715  cvmliftlem10  23825  sinccvglem  24005  axlowdimlem4  24573  axlowdimlem6  24575  axlowdimlem10  24579  axlowdimlem11  24580  axlowdimlem12  24581  axlowdim1  24587  phckle  26027  psckle  26028  pgapspf  26052  pgapspf2  26053  rabren3dioph  26898  2nn0ind  27030  flcidc  27379  cnmsgnsubg  27434  dvsid  27548  refsum2cnlem1  27708  itgsin0pilem1  27744  sgnval  28245
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264  ax-1cn 8795
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-v 2790
  Copyright terms: Public domain W3C validator