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

Theorem 1ex 9663
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 9622 . 2  |-  1  e.  CC
21elexi 3066 1  |-  1  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1897   _Vcvv 3056   CCcc 9562   1c1 9565
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-12 1943  ax-ext 2441  ax-1cn 9622
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-v 3058
This theorem is referenced by:  1nn  10647  dfnn2  10649  nn1suc  10657  nn0ind-raph  11063  fzprval  11884  fztpval  11885  expval  12305  m1expcl2  12325  1exp  12332  facnn  12492  fac0  12493  prhash2ex  12607  funcnvs2  13043  funcnvs3  13044  funcnvs4  13045  wrdlen2i  13066  wrd2pr2op  13067  wrd3tpop  13071  wwlktovf1  13080  relexp1g  13137  dfid6  13139  sgnval  13199  harmonic  13965  prodf1f  13996  fprodntriv  14044  prod1  14046  fprodss  14050  fprodn0f  14093  ege2le3  14192  ruclem8  14337  ruclem11  14340  1nprm  14677  isprm2lem  14679  pcmpt  14885  mgmnsgrpex  16713  pmtrprfval  17176  pmtrprfvalrn  17177  psgnprfval  17210  psgnprfval1  17211  abvtrivd  18116  cnmsgnsubg  19193  m2detleiblem1  19697  m2detleiblem5  19698  m2detleiblem6  19699  m2detleiblem3  19702  m2detleiblem4  19703  m2detleib  19704  imasdsf1olem  21436  pcopt  22101  pcopt2  22102  pcoass  22103  voliunlem1  22551  i1f1lem  22695  i1f1  22696  itg11  22697  iblcnlem1  22793  bddibl  22845  dvexp  22955  mvth  22992  iaa  23329  aalioulem2  23337  efrlim  23943  amgmlem  23963  amgm  23964  wilthlem2  24042  wilthlem3  24043  basellem7  24061  basellem9  24063  ppiublem2  24179  pclogsum  24191  bposlem5  24264  lgsfval  24277  lgsdir2lem3  24301  lgsdir  24306  lgsdilem2  24307  lgsdi  24308  lgsne0  24309  ostth1  24519  istrkg2ld  24556  axlowdimlem4  25023  axlowdimlem6  25025  axlowdimlem10  25029  axlowdimlem11  25030  axlowdimlem12  25031  axlowdimlem13  25032  axlowdim1  25037  2trllemH  25330  2trllemE  25331  2wlklemB  25333  wlkntrllem1  25337  wlkntrllem2  25338  wlkntrllem3  25339  2wlklem  25342  constr1trl  25366  1pthon  25369  2pthlem1  25373  2pthlem2  25374  2wlklem1  25375  usgra2wlkspthlem1  25395  usgra2wlkspthlem2  25396  constr3lem2  25422  constr3lem4  25423  constr3lem5  25424  constr3trllem1  25426  constr3trllem2  25427  el2wlkonotlem  25638  usg2wlkonot  25659  usg2wotspth  25660  ex-xp  25934  nmopun  27715  pjnmopi  27849  iuninc  28224  sgnsval  28539  sgnsf  28540  psgnid  28658  cntnevol  29098  ddeval1  29105  ddeval0  29106  eulerpartgbij  29253  coinfliprv  29363  sgncl  29457  subfacp1lem1  29950  subfacp1lem2a  29951  subfacp1lem3  29953  subfacp1lem5  29955  cvmliftlem10  30065  sinccvglem  30364  poimirlem1  31985  poimirlem2  31986  poimirlem3  31987  poimirlem4  31988  poimirlem6  31990  poimirlem7  31991  poimirlem10  31994  poimirlem11  31995  poimirlem12  31996  poimirlem16  32000  poimirlem17  32001  poimirlem19  32003  poimirlem20  32004  poimirlem23  32007  poimirlem24  32008  poimirlem25  32009  poimirlem28  32012  poimirlem29  32013  poimirlem31  32015  itg2addnclem  32037  rabren3dioph  35702  2nn0ind  35837  flcidc  36084  dfrcl4  36312  fvilbdRP  36326  fvrcllb1d  36331  iunrelexp0  36338  corclrcl  36343  relexp1idm  36350  cotrcltrcl  36361  trclfvdecomr  36364  corcltrcl  36375  cotrclrcl  36378  dvsid  36723  binomcxplemnotnn0  36748  refsum2cnlem1  37397  itgsin0pilem1  37863  fourierdlem29  38035  fourierdlem56  38063  fourierdlem62  38069  fourierswlem  38131  fouriersw  38132  nnsum3primes4  38920  nnsum3primesgbe  38924  nnsum4primesodd  38928  nnsum4primesoddALTV  38929  fun2dmnopgexmpl  39069  umgr2v2eedg  39610  umgr2v2e  39611  umgr2v2evd2  39613  2Wlklem  39713  usgr2wlkneq  39787  21wlkdlem4  39876  21wlkdlem5  39877  2pthdlem1  39878  21wlkdlem10  39883  31wlkdlem4  39902  31wlkdlem5  39903  3pthdlem1  39904  31wlkdlem10  39909  upgr3v3e3cycl  39920  upgr4cycl4dv4e  39925  usgra2pthspth  39937  usgra2adedglem1  39942  zlmodzxzel  40408  zlmodzxz0  40409  zlmodzxzscm  40410  zlmodzxzadd  40411  blenval  40654  nn0sumshdiglemB  40703
  Copyright terms: Public domain W3C validator