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

Theorem 1ex 9590
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 9549 . 2  |-  1  e.  CC
21elexi 3123 1  |-  1  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1767   _Vcvv 3113   CCcc 9489   1c1 9492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803  ax-ext 2445  ax-1cn 9549
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-v 3115
This theorem is referenced by:  1nn  10546  dfnn2  10548  nn1suc  10556  nn0ind-raph  10960  fzprval  11739  fztpval  11740  expval  12135  m1expcl2  12155  1exp  12162  facnn  12322  fac0  12323  wrdlen2i  12846  wrd2pr2op  12847  wwlktovf1  12857  sgnval  12883  harmonic  13632  ege2le3  13686  ruclem8  13830  ruclem11  13833  1nprm  14080  isprm2lem  14082  pcmpt  14269  pmtrprfval  16315  pmtrprfvalrn  16316  psgnprfval  16349  psgnprfval1  16350  abvtrivd  17284  cnmsgnsubg  18396  m2detleiblem1  18909  m2detleiblem5  18910  m2detleiblem6  18911  m2detleiblem3  18914  m2detleiblem4  18915  m2detleib  18916  imasdsf1olem  20627  pcopt  21273  pcopt2  21274  pcoass  21275  voliunlem1  21711  i1f1lem  21847  i1f1  21848  itg11  21849  iblcnlem1  21945  bddibl  21997  dvexp  22107  mvth  22144  aalioulem2  22479  efrlim  23043  amgmlem  23063  amgm  23064  wilthlem2  23087  wilthlem3  23088  basellem7  23104  basellem9  23106  ppiublem2  23222  pclogsum  23234  perfectlem2  23249  bposlem5  23307  lgsfval  23320  lgsdir2lem3  23344  lgsdir  23349  lgsdilem2  23350  lgsdi  23351  lgsne0  23352  ostth1  23562  istrkg2ld  23602  axlowdimlem4  23940  axlowdimlem6  23942  axlowdimlem10  23946  axlowdimlem11  23947  axlowdimlem12  23948  axlowdim1  23954  2trllemH  24246  2trllemE  24247  2wlklemB  24249  wlkntrllem1  24253  wlkntrllem2  24254  wlkntrllem3  24255  2wlklem  24258  constr1trl  24282  1pthon  24285  2pthlem1  24289  2pthlem2  24290  2wlklem1  24291  usgra2wlkspthlem1  24311  usgra2wlkspthlem2  24312  constr3lem2  24338  constr3lem4  24339  constr3lem5  24340  constr3trllem1  24342  constr3trllem2  24343  el2wlkonotlem  24554  usg2wlkonot  24575  usg2wotspth  24576  ex-xp  24850  nmopun  26625  pjnmopi  26759  iuninc  27117  sgnsval  27396  sgnsf  27397  cntnevol  27855  ddeval1  27862  ddeval0  27863  eulerpartgbij  27967  coinfliprv  28077  sgncl  28133  subfacp1lem1  28279  subfacp1lem2a  28280  subfacp1lem3  28282  subfacp1lem5  28284  cvmliftlem10  28395  sinccvglem  28529  prodf1f  28619  fprodntriv  28667  prod1  28669  fprodss  28673  itg2addnclem  29659  rabren3dioph  30369  2nn0ind  30501  flcidc  30744  dvsid  30852  refsum2cnlem1  31006  itgsin0pilem1  31283  fourierdlem29  31452  fourierdlem56  31479  fourierdlem62  31485  fourierswlem  31547  fouriersw  31548  usgra2pthspth  31834  usgra2pthlem1  31836  usgra2pth  31837  usgra2adedglem1  31839  zlmodzxzel  32028  zlmodzxz0  32029  zlmodzxzscm  32030  zlmodzxzadd  32031
  Copyright terms: Public domain W3C validator