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

Theorem 1ex 9381
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 9340 . 2  |-  1  e.  CC
21elexi 2982 1  |-  1  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   _Vcvv 2972   CCcc 9280   1c1 9283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423  ax-1cn 9340
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-v 2974
This theorem is referenced by:  1nn  10333  dfnn2  10335  nn1suc  10343  nn0ind-raph  10742  fzprval  11517  fztpval  11518  expval  11867  m1expcl2  11887  1exp  11893  facnn  12053  fac0  12054  wrdlen2i  12546  wrd2pr2op  12547  sgnval  12577  harmonic  13321  ege2le3  13375  ruclem8  13519  ruclem11  13522  1nprm  13768  isprm2lem  13770  pcmpt  13954  pmtrprfval  15993  pmtrprfvalrn  15994  psgnprfval  16025  psgnprfval1  16026  abvtrivd  16925  cnmsgnsubg  18007  m2detleiblem1  18430  m2detleiblem5  18431  m2detleiblem6  18432  m2detleiblem3  18435  m2detleiblem4  18436  m2detleib  18437  imasdsf1olem  19948  pcopt  20594  pcopt2  20595  pcoass  20596  voliunlem1  21031  i1f1lem  21167  i1f1  21168  itg11  21169  iblcnlem1  21265  bddibl  21317  dvexp  21427  mvth  21464  aalioulem2  21799  efrlim  22363  amgmlem  22383  amgm  22384  wilthlem2  22407  wilthlem3  22408  basellem7  22424  basellem9  22426  ppiublem2  22542  pclogsum  22554  perfectlem2  22569  bposlem5  22627  lgsfval  22640  lgsdir2lem3  22664  lgsdir  22669  lgsdilem2  22670  lgsdi  22671  lgsne0  22672  ostth1  22882  axlowdimlem4  23191  axlowdimlem6  23193  axlowdimlem10  23197  axlowdimlem11  23198  axlowdimlem12  23199  axlowdim1  23205  2trllemH  23451  2trllemE  23452  2wlklemB  23454  wlkntrllem1  23458  wlkntrllem2  23459  wlkntrllem3  23460  2wlklem  23463  constr1trl  23487  1pthon  23490  2pthlem1  23494  2pthlem2  23495  2wlklem1  23496  constr3lem2  23532  constr3lem4  23533  constr3lem5  23534  constr3trllem1  23536  constr3trllem2  23537  ex-xp  23643  nmopun  25418  pjnmopi  25552  iuninc  25911  sgnsval  26191  sgnsf  26192  cntnevol  26642  ddeval1  26650  ddeval0  26651  eulerpartgbij  26755  coinfliprv  26865  sgncl  26921  subfacp1lem1  27067  subfacp1lem2a  27068  subfacp1lem3  27070  subfacp1lem5  27072  cvmliftlem10  27183  sinccvglem  27317  prodf1f  27407  fprodntriv  27455  prod1  27457  fprodss  27461  itg2addnclem  28443  rabren3dioph  29154  2nn0ind  29286  flcidc  29531  dvsid  29605  refsum2cnlem1  29759  itgsin0pilem1  29790  wwlktovf1  30252  usgra2pthspth  30295  usgra2wlkspthlem1  30296  usgra2wlkspthlem2  30297  usgra2pthlem1  30300  usgra2pth  30301  usgra2adedglem1  30308  el2wlkonotlem  30381  usg2wlkonot  30402  usg2wotspth  30403  zlmodzxzel  30752  zlmodzxz0  30753  zlmodzxzscm  30754  zlmodzxzadd  30755
  Copyright terms: Public domain W3C validator