Theorem 1ex 9612

Description: 1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.)

Assertion

Ref	Expression
1ex

Proof of Theorem 1ex

Step	Hyp	Ref	Expression
1		ax-1cn 9571	. 2
2	1	elexi 3119	1

Syntax hints:  e.wcel 1818  cvv 3109  cc 9511  1c1 9514

This theorem is referenced by:  1nn  10572  dfnn2  10574  nn1suc  10582  nn0ind-raph  10989  fzprval  11769  fztpval  11770  expval  12168  m1expcl2  12188  1exp  12195  facnn  12355  fac0  12356  prhash2ex  12464  wrdlen2i  12884  wrd2pr2op  12885  wwlktovf1  12895  sgnval  12921  harmonic  13670  prodf1f  13701  fprodntriv  13749  prod1  13751  fprodss  13755  ege2le3  13825  ruclem8  13970  ruclem11  13973  1nprm  14222  isprm2lem  14224  pcmpt  14411  mgmnsgrpex  16049  pmtrprfval  16512  pmtrprfvalrn  16513  psgnprfval  16546  psgnprfval1  16547  abvtrivd  17489  cnmsgnsubg  18613  m2detleiblem1  19126  m2detleiblem5  19127  m2detleiblem6  19128  m2detleiblem3  19131  m2detleiblem4  19132  m2detleib  19133  imasdsf1olem  20876  pcopt  21522  pcopt2  21523  pcoass  21524  voliunlem1  21960  i1f1lem  22096  i1f1  22097  itg11  22098  iblcnlem1  22194  bddibl  22246  dvexp  22356  mvth  22393  iaa  22721  aalioulem2  22729  efrlim  23299  amgmlem  23319  amgm  23320  wilthlem2  23343  wilthlem3  23344  basellem7  23360  basellem9  23362  ppiublem2  23478  pclogsum  23490  bposlem5  23563  lgsfval  23576  lgsdir2lem3  23600  lgsdir  23605  lgsdilem2  23606  lgsdi  23607  lgsne0  23608  ostth1  23818  istrkg2ld  23858  axlowdimlem4  24248  axlowdimlem6  24250  axlowdimlem10  24254  axlowdimlem11  24255  axlowdimlem12  24256  axlowdimlem13  24257  axlowdim1  24262  2trllemH  24554  2trllemE  24555  2wlklemB  24557  wlkntrllem1  24561  wlkntrllem2  24562  wlkntrllem3  24563  2wlklem  24566  constr1trl  24590  1pthon  24593  2pthlem1  24597  2pthlem2  24598  2wlklem1  24599  usgra2wlkspthlem1  24619  usgra2wlkspthlem2  24620  constr3lem2  24646  constr3lem4  24647  constr3lem5  24648  constr3trllem1  24650  constr3trllem2  24651  el2wlkonotlem  24862  usg2wlkonot  24883  usg2wotspth  24884  ex-xp  25157  nmopun  26933  pjnmopi  27067  iuninc  27428  sgnsval  27718  sgnsf  27719  cntnevol  28199  ddeval1  28206  ddeval0  28207  eulerpartgbij  28311  coinfliprv  28421  sgncl  28477  subfacp1lem1  28623  subfacp1lem2a  28624  subfacp1lem3  28626  subfacp1lem5  28628  cvmliftlem10  28739  sinccvglem  29038  itg2addnclem  30066  rabren3dioph  30749  2nn0ind  30881  flcidc  31123  dvsid  31236  binomcxplemnotnn0  31261  refsum2cnlem1  31412  fprodn0f  31594  itgsin0pilem1  31748  fourierdlem29  31918  fourierdlem56  31945  fourierdlem62  31951  fourierswlem  32013  fouriersw  32014  usgra2pthspth  32351  usgra2adedglem1  32356  zlmodzxzel  32944  zlmodzxz0  32945  zlmodzxzscm  32946  zlmodzxzadd  32947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854  ax-ext 2435  ax-1cn 9571

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111