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

Theorem 1ex 9637
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 9596 . 2  |-  1  e.  CC
21elexi 3097 1  |-  1  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1870   _Vcvv 3087   CCcc 9536   1c1 9539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-12 1907  ax-ext 2407  ax-1cn 9596
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-v 3089
This theorem is referenced by:  1nn  10620  dfnn2  10622  nn1suc  10630  nn0ind-raph  11035  fzprval  11854  fztpval  11855  expval  12271  m1expcl2  12291  1exp  12298  facnn  12458  fac0  12459  prhash2ex  12573  wrdlen2i  13000  wrd2pr2op  13001  wwlktovf1  13011  relexp1g  13068  dfid6  13070  sgnval  13130  harmonic  13895  prodf1f  13926  fprodntriv  13974  prod1  13976  fprodss  13980  fprodn0f  14023  ege2le3  14122  ruclem8  14267  ruclem11  14270  1nprm  14600  isprm2lem  14602  pcmpt  14800  mgmnsgrpex  16616  pmtrprfval  17079  pmtrprfvalrn  17080  psgnprfval  17113  psgnprfval1  17114  abvtrivd  18003  cnmsgnsubg  19076  m2detleiblem1  19580  m2detleiblem5  19581  m2detleiblem6  19582  m2detleiblem3  19585  m2detleiblem4  19586  m2detleib  19587  imasdsf1olem  21319  pcopt  21946  pcopt2  21947  pcoass  21948  voliunlem1  22380  i1f1lem  22524  i1f1  22525  itg11  22526  iblcnlem1  22622  bddibl  22674  dvexp  22784  mvth  22821  iaa  23146  aalioulem2  23154  efrlim  23760  amgmlem  23780  amgm  23781  wilthlem2  23859  wilthlem3  23860  basellem7  23876  basellem9  23878  ppiublem2  23994  pclogsum  24006  bposlem5  24079  lgsfval  24092  lgsdir2lem3  24116  lgsdir  24121  lgsdilem2  24122  lgsdi  24123  lgsne0  24124  ostth1  24334  istrkg2ld  24371  axlowdimlem4  24821  axlowdimlem6  24823  axlowdimlem10  24827  axlowdimlem11  24828  axlowdimlem12  24829  axlowdimlem13  24830  axlowdim1  24835  2trllemH  25127  2trllemE  25128  2wlklemB  25130  wlkntrllem1  25134  wlkntrllem2  25135  wlkntrllem3  25136  2wlklem  25139  constr1trl  25163  1pthon  25166  2pthlem1  25170  2pthlem2  25171  2wlklem1  25172  usgra2wlkspthlem1  25192  usgra2wlkspthlem2  25193  constr3lem2  25219  constr3lem4  25220  constr3lem5  25221  constr3trllem1  25223  constr3trllem2  25224  el2wlkonotlem  25435  usg2wlkonot  25456  usg2wotspth  25457  ex-xp  25731  nmopun  27502  pjnmopi  27636  iuninc  28015  sgnsval  28329  sgnsf  28330  psgnid  28449  cntnevol  28889  ddeval1  28896  ddeval0  28897  eulerpartgbij  29031  coinfliprv  29141  sgncl  29197  subfacp1lem1  29690  subfacp1lem2a  29691  subfacp1lem3  29693  subfacp1lem5  29695  cvmliftlem10  29805  sinccvglem  30104  poimirlem1  31645  poimirlem2  31646  poimirlem3  31647  poimirlem4  31648  poimirlem6  31650  poimirlem7  31651  poimirlem10  31654  poimirlem11  31655  poimirlem12  31656  poimirlem16  31660  poimirlem17  31661  poimirlem19  31663  poimirlem20  31664  poimirlem23  31667  poimirlem24  31668  poimirlem25  31669  poimirlem28  31672  poimirlem29  31673  poimirlem31  31675  itg2addnclem  31697  rabren3dioph  35367  2nn0ind  35499  flcidc  35739  dfrcl4  35907  fvilbdRP  35921  fvrcllb1d  35926  iunrelexp0  35933  corclrcl  35938  relexp1idm  35945  cotrcltrcl  35956  trclfvdecomr  35959  corcltrcl  35970  cotrclrcl  35973  dvsid  36317  binomcxplemnotnn0  36342  refsum2cnlem1  36998  itgsin0pilem1  37395  fourierdlem29  37567  fourierdlem56  37594  fourierdlem62  37600  fourierswlem  37662  fouriersw  37663  nnsum3primes4  38273  nnsum3primesgbe  38277  nnsum4primesodd  38281  nnsum4primesoddALTV  38282  usgra2pthspth  38421  usgra2adedglem1  38426  zlmodzxzel  38896  zlmodzxz0  38897  zlmodzxzscm  38898  zlmodzxzadd  38899  blenval  39143  nn0sumshdiglemB  39192
  Copyright terms: Public domain W3C validator