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

Theorem 1ex 9582
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 9541 . 2  |-  1  e.  CC
21elexi 3026 1  |-  1  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1872   _Vcvv 3016   CCcc 9481   1c1 9484
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-12 1909  ax-ext 2402  ax-1cn 9541
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-sb 1791  df-clab 2409  df-cleq 2415  df-clel 2418  df-v 3018
This theorem is referenced by:  1nn  10564  dfnn2  10566  nn1suc  10574  nn0ind-raph  10979  fzprval  11800  fztpval  11801  expval  12217  m1expcl2  12237  1exp  12244  facnn  12404  fac0  12405  prhash2ex  12519  wrdlen2i  12958  wrd2pr2op  12959  wwlktovf1  12969  relexp1g  13026  dfid6  13028  sgnval  13088  harmonic  13853  prodf1f  13884  fprodntriv  13932  prod1  13934  fprodss  13938  fprodn0f  13981  ege2le3  14080  ruclem8  14225  ruclem11  14228  1nprm  14565  isprm2lem  14567  pcmpt  14773  mgmnsgrpex  16601  pmtrprfval  17064  pmtrprfvalrn  17065  psgnprfval  17098  psgnprfval1  17099  abvtrivd  18004  cnmsgnsubg  19080  m2detleiblem1  19584  m2detleiblem5  19585  m2detleiblem6  19586  m2detleiblem3  19589  m2detleiblem4  19590  m2detleib  19591  imasdsf1olem  21323  pcopt  21988  pcopt2  21989  pcoass  21990  voliunlem1  22438  i1f1lem  22582  i1f1  22583  itg11  22584  iblcnlem1  22680  bddibl  22732  dvexp  22842  mvth  22879  iaa  23216  aalioulem2  23224  efrlim  23830  amgmlem  23850  amgm  23851  wilthlem2  23929  wilthlem3  23930  basellem7  23948  basellem9  23950  ppiublem2  24066  pclogsum  24078  bposlem5  24151  lgsfval  24164  lgsdir2lem3  24188  lgsdir  24193  lgsdilem2  24194  lgsdi  24195  lgsne0  24196  ostth1  24406  istrkg2ld  24443  axlowdimlem4  24910  axlowdimlem6  24912  axlowdimlem10  24916  axlowdimlem11  24917  axlowdimlem12  24918  axlowdimlem13  24919  axlowdim1  24924  2trllemH  25217  2trllemE  25218  2wlklemB  25220  wlkntrllem1  25224  wlkntrllem2  25225  wlkntrllem3  25226  2wlklem  25229  constr1trl  25253  1pthon  25256  2pthlem1  25260  2pthlem2  25261  2wlklem1  25262  usgra2wlkspthlem1  25282  usgra2wlkspthlem2  25283  constr3lem2  25309  constr3lem4  25310  constr3lem5  25311  constr3trllem1  25313  constr3trllem2  25314  el2wlkonotlem  25525  usg2wlkonot  25546  usg2wotspth  25547  ex-xp  25821  nmopun  27602  pjnmopi  27736  iuninc  28115  sgnsval  28435  sgnsf  28436  psgnid  28555  cntnevol  28995  ddeval1  29002  ddeval0  29003  eulerpartgbij  29150  coinfliprv  29260  sgncl  29354  subfacp1lem1  29847  subfacp1lem2a  29848  subfacp1lem3  29850  subfacp1lem5  29852  cvmliftlem10  29962  sinccvglem  30261  poimirlem1  31842  poimirlem2  31843  poimirlem3  31844  poimirlem4  31845  poimirlem6  31847  poimirlem7  31848  poimirlem10  31851  poimirlem11  31852  poimirlem12  31853  poimirlem16  31857  poimirlem17  31858  poimirlem19  31860  poimirlem20  31861  poimirlem23  31864  poimirlem24  31865  poimirlem25  31866  poimirlem28  31869  poimirlem29  31870  poimirlem31  31872  itg2addnclem  31894  rabren3dioph  35564  2nn0ind  35700  flcidc  35947  dfrcl4  36175  fvilbdRP  36189  fvrcllb1d  36194  iunrelexp0  36201  corclrcl  36206  relexp1idm  36213  cotrcltrcl  36224  trclfvdecomr  36227  corcltrcl  36238  cotrclrcl  36241  dvsid  36587  binomcxplemnotnn0  36612  refsum2cnlem1  37268  itgsin0pilem1  37703  fourierdlem29  37875  fourierdlem56  37903  fourierdlem62  37909  fourierswlem  37971  fouriersw  37972  nnsum3primes4  38690  nnsum3primesgbe  38694  nnsum4primesodd  38698  nnsum4primesoddALTV  38699  fun2dmnopgexmpl  38828  usgra2pthspth  39250  usgra2adedglem1  39255  zlmodzxzel  39723  zlmodzxz0  39724  zlmodzxzscm  39725  zlmodzxzadd  39726  blenval  39969  nn0sumshdiglemB  40018
  Copyright terms: Public domain W3C validator