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

Theorem 1ex 9086
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 9048 . 2  |-  1  e.  CC
21elexi 2965 1  |-  1  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1725   _Vcvv 2956   CCcc 8988   1c1 8991
This theorem is referenced by:  1nn  10011  dfnn2  10013  nn1suc  10021  nn0ind-raph  10370  fzprval  11106  fztpval  11107  expval  11384  m1expcl2  11403  1exp  11409  facnn  11568  fac0  11569  harmonic  12638  ege2le3  12692  ruclem8  12836  ruclem11  12839  1nprm  13084  isprm2lem  13086  pcmpt  13261  abvtrivd  15928  imasdsf1olem  18403  pcopt  19047  pcopt2  19048  pcoass  19049  voliunlem1  19444  i1f1lem  19581  i1f1  19582  itg11  19583  iblcnlem1  19679  bddibl  19731  dvexp  19839  mvth  19876  aalioulem2  20250  efrlim  20808  basellem7  20869  basellem9  20871  ppiublem2  20987  pclogsum  20999  perfectlem2  21014  bposlem5  21072  lgsfval  21085  lgsdir2lem3  21109  lgsdir  21114  lgsdilem2  21115  lgsdi  21116  lgsne0  21117  ostth1  21327  2trllemH  21552  2trllemE  21553  2wlklemB  21555  wlkntrllem1  21559  wlkntrllem2  21560  wlkntrllem3  21561  2wlklem  21564  constr1trl  21588  1pthon  21591  2pthlem1  21595  2pthlem2  21596  2wlklem1  21597  constr3lem2  21633  constr3lem4  21634  constr3lem5  21635  constr3trllem1  21637  constr3trllem2  21638  ex-xp  21744  nmopun  23517  pjnmopi  23651  iuninc  24011  cntnevol  24582  coinfliprv  24740  subfacp1lem1  24865  subfacp1lem2a  24866  subfacp1lem3  24868  subfacp1lem5  24870  cvmliftlem10  24981  sinccvglem  25109  prodf1f  25220  fprodntriv  25268  prod1  25270  fprodss  25274  axlowdimlem4  25884  axlowdimlem6  25886  axlowdimlem10  25890  axlowdimlem11  25891  axlowdimlem12  25892  axlowdim1  25898  itg2addnclem  26256  ftc1anclem8  26287  rabren3dioph  26876  2nn0ind  27008  flcidc  27356  cnmsgnsubg  27411  dvsid  27525  refsum2cnlem1  27684  itgsin0pilem1  27720  usgra2pthspth  28305  usgra2wlkspthlem1  28306  usgra2wlkspthlem2  28307  usgra2pthlem1  28310  usgra2pth  28311  usgra2adedglem1  28318  el2wlkonotlem  28329  usg2wlkonot  28350  usg2wotspth  28351  sgnval  28518
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417  ax-1cn 9048
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-v 2958
  Copyright terms: Public domain W3C validator