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

Theorem 1ex 9580
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 9539 . 2  |-  1  e.  CC
21elexi 3116 1  |-  1  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1823   _Vcvv 3106   CCcc 9479   1c1 9482
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-12 1859  ax-ext 2432  ax-1cn 9539
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3108
This theorem is referenced by:  1nn  10542  dfnn2  10544  nn1suc  10552  nn0ind-raph  10960  fzprval  11744  fztpval  11745  expval  12150  m1expcl2  12170  1exp  12177  facnn  12337  fac0  12338  prhash2ex  12448  wrdlen2i  12875  wrd2pr2op  12876  wwlktovf1  12886  relexp1g  12943  sgnval  13003  harmonic  13752  prodf1f  13783  fprodntriv  13831  prod1  13833  fprodss  13837  ege2le3  13907  ruclem8  14054  ruclem11  14057  1nprm  14306  isprm2lem  14308  pcmpt  14495  mgmnsgrpex  16248  pmtrprfval  16711  pmtrprfvalrn  16712  psgnprfval  16745  psgnprfval1  16746  abvtrivd  17684  cnmsgnsubg  18786  m2detleiblem1  19293  m2detleiblem5  19294  m2detleiblem6  19295  m2detleiblem3  19298  m2detleiblem4  19299  m2detleib  19300  imasdsf1olem  21042  pcopt  21688  pcopt2  21689  pcoass  21690  voliunlem1  22126  i1f1lem  22262  i1f1  22263  itg11  22264  iblcnlem1  22360  bddibl  22412  dvexp  22522  mvth  22559  iaa  22887  aalioulem2  22895  efrlim  23497  amgmlem  23517  amgm  23518  wilthlem2  23541  wilthlem3  23542  basellem7  23558  basellem9  23560  ppiublem2  23676  pclogsum  23688  bposlem5  23761  lgsfval  23774  lgsdir2lem3  23798  lgsdir  23803  lgsdilem2  23804  lgsdi  23805  lgsne0  23806  ostth1  24016  istrkg2ld  24056  axlowdimlem4  24450  axlowdimlem6  24452  axlowdimlem10  24456  axlowdimlem11  24457  axlowdimlem12  24458  axlowdimlem13  24459  axlowdim1  24464  2trllemH  24756  2trllemE  24757  2wlklemB  24759  wlkntrllem1  24763  wlkntrllem2  24764  wlkntrllem3  24765  2wlklem  24768  constr1trl  24792  1pthon  24795  2pthlem1  24799  2pthlem2  24800  2wlklem1  24801  usgra2wlkspthlem1  24821  usgra2wlkspthlem2  24822  constr3lem2  24848  constr3lem4  24849  constr3lem5  24850  constr3trllem1  24852  constr3trllem2  24853  el2wlkonotlem  25064  usg2wlkonot  25085  usg2wotspth  25086  ex-xp  25359  nmopun  27131  pjnmopi  27265  iuninc  27638  sgnsval  27952  sgnsf  27953  cntnevol  28436  ddeval1  28443  ddeval0  28444  eulerpartgbij  28575  coinfliprv  28685  sgncl  28741  subfacp1lem1  28887  subfacp1lem2a  28888  subfacp1lem3  28890  subfacp1lem5  28892  cvmliftlem10  29003  sinccvglem  29302  itg2addnclem  30306  rabren3dioph  30988  2nn0ind  31120  flcidc  31364  dvsid  31477  binomcxplemnotnn0  31502  refsum2cnlem1  31652  fprodn0f  31833  itgsin0pilem1  31987  fourierdlem29  32157  fourierdlem56  32184  fourierdlem62  32190  fourierswlem  32252  fouriersw  32253  usgra2pthspth  32723  usgra2adedglem1  32728  zlmodzxzel  33198  zlmodzxz0  33199  zlmodzxzscm  33200  zlmodzxzadd  33201  blenval  33446  nn0sumshdiglemB  33495  dfid6  38196  dfrcl4  38197  relexp1idm  38221  iunrelexp0  38224  corclrcl  38230  corcltrcl  38231  cotrclrcl  38232  cotrcltrcl  38233
  Copyright terms: Public domain W3C validator