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

Theorem 1ex 8849
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 8811 . 2  |-  1  e.  CC
21elexi 2810 1  |-  1  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1696   _Vcvv 2801   CCcc 8751   1c1 8754
This theorem is referenced by:  1nn  9773  dfnn2  9775  nn1suc  9783  nn0ind-raph  10128  fzprval  10860  fztpval  10861  expval  11122  m1expcl2  11141  1exp  11147  facnn  11306  fac0  11307  harmonic  12333  ege2le3  12387  ruclem8  12531  1nprm  12779  isprm2lem  12781  pcmpt  12956  abvtrivd  15621  imasdsf1olem  17953  pcopt  18536  pcopt2  18537  pcoass  18538  voliunlem1  18923  i1f1lem  19060  i1f1  19061  itg11  19062  iblcnlem1  19158  bddibl  19210  dvexp  19318  mvth  19355  aalioulem2  19729  efrlim  20280  basellem7  20340  basellem9  20342  ppiublem2  20458  pclogsum  20470  perfectlem2  20485  bposlem5  20543  lgsfval  20556  lgsdir2lem3  20580  lgsdir  20585  lgsdilem2  20586  lgsdi  20587  lgsne0  20588  ostth1  20798  ex-xp  20839  nmopun  22610  pjnmopi  22744  cntnevol  23191  coinfliprv  23698  subfacp1lem1  23725  subfacp1lem2a  23726  subfacp1lem3  23728  subfacp1lem5  23730  cvmliftlem10  23840  sinccvglem  24020  faclimlem3  24119  prodf1f  24166  cprod0  24168  prod1  24169  axlowdimlem4  24645  axlowdimlem6  24647  axlowdimlem10  24651  axlowdimlem11  24652  axlowdimlem12  24653  axlowdim1  24659  itg2addnclem  25003  itg2addnc  25005  phckle  26130  psckle  26131  pgapspf  26155  pgapspf2  26156  rabren3dioph  27001  2nn0ind  27133  flcidc  27482  cnmsgnsubg  27537  dvsid  27651  refsum2cnlem1  27811  itgsin0pilem1  27847  wlkntrllem1  28345  wlkntrllem3  28347  wlkntrllem4  28348  wlkntrllem5  28349  constr3lem2  28392  constr3lem4  28393  constr3lem5  28394  constr3trllem1  28396  constr3trllem2  28397  sgnval  28499
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277  ax-1cn 8811
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-v 2803
  Copyright terms: Public domain W3C validator