Theorem rspcev 3590

Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2182, ax-11 2198, ax-12 2219. (Revised by SN, 12-Dec-2023.)

Hypothesis

Ref	Expression
rspcv.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rspcev	⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspcev

Step	Hyp	Ref	Expression
1		id 23	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ 𝐵)
2		rspcv.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	adantl 486	. . 3 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓))
4	1, 3	rspcedv 3583	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝜓 → ∃𝑥 ∈ 𝐵 𝜑))
5	4	imp 411	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096

This theorem is referenced by:  rspcedvdw  3593  rspceaimv  3596  rspc2ev  3603  rspc3ev  3607  rspceeqv  3613  reu6i  3700  rspesbca  3843  eliuni  4966  iuneqconst  4972  brralrspcev  5175  wefrc  5656  wereu2  5659  xpdifid  6166  xpdifcnvepel  6167  frpomin  6342  onfr  6401  onelssex  6411  ordunidif  6412  eliman0  6919  dffv2  6977  elrnrexdm  7085  eldmrexrn  7087  elabrex  7241  elabrexg  7242  f1elima  7262  fliftfun  7311  fliftval  7315  f1oiso2  7351  sorpssuni  7730  sorpssint  7731  onssmin  7791  onminex  7801  fimaproj  8131  frxp3  8147  poseq  8154  tfrlem12  8376  seqomlem2  8438  oawordeulem  8539  oaass  8546  odi  8564  omass  8565  omeulem1  8567  oen0  8572  oelim2  8581  oeeulem  8587  nnawordex  8623  nnaordex2  8625  eldifsucnn  8650  cofon1  8658  cofon2  8659  naddcllem  8662  naddunif  8680  boxcutc  8939  0fi  9039  snfi  9040  rexdif1en  9145  findcard  9148  nnfi  9152  pssnn  9153  unfi  9155  onfin  9199  dif1ennnALT  9237  frfi  9245  fisupg  9248  nnsdomg  9259  pwfir  9276  prfi  9283  fissuni  9314  fipreima  9315  finsschain  9316  indexfi  9317  marypha1lem  9393  eqsup  9416  supmax  9428  fisup2g  9429  fisupcl  9430  supisoex  9435  infmin  9456  fiinfg  9461  fiinf2g  9462  wofib  9507  wemaplem2  9509  card2inf  9517  brwdom2  9535  cnfcom3clem  9674  ssttrcl  9684  ttrcltr  9685  trcl  9697  frmin  9721  r1ordg  9750  r1pwss  9756  tz9.12lem3  9761  tz9.12  9762  r1elwf  9768  tcrank  9856  scottex  9859  scott0  9860  isnumi  9932  onsdom  9982  ondomen  10021  infpwfien  10046  cardaleph  10073  infenaleph  10075  alephfplem4  10091  alephfp2  10093  dfac2b  10114  ackbij1lem18  10219  ackbij1  10220  cflem  10228  cflemOLD  10229  cflecard  10236  cfsuc  10241  cfflb  10243  cofsmo  10253  coftr  10257  fin23lem7  10300  fin23lem11  10301  enfin2i  10305  fin23lem26  10309  isf32lem5  10341  isf34lem4  10361  isfin1-3  10370  fin1a2lem7  10390  axdc3lem4  10437  ttukeylem7  10499  iunfo  10523  ficard  10549  pwcfsdom  10568  fpwwe2lem11  10626  wunex  10724  eltsk2g  10736  grur1  10805  axgroth6  10813  inaprc  10821  nqereu  10914  archnq  10965  genpnmax  10992  ltexpri  11028  prlem936  11032  recexpr  11036  supexpr  11039  negexsr  11087  recexsrlem  11088  recexsr  11092  supsrlem  11096  axrnegex  11147  axrrecex  11148  axpre-sup  11154  1re  11208  dedekind  11373  dedekindle  11374  cnegex  11391  cnegex2  11392  recex  11846  receu  11859  fiminre2  12163  cju  12214  nn2ge  12263  nominpos  12481  zdiv  12666  btwnz  12699  uzwo  12935  ublbneg  12957  lbzbi  12960  zsupss  12961  uzsupss  12964  rpnnen1lem1  13002  rpnnen1lem3  13003  rpnnen1lem4  13004  rpnnen1lem5  13005  z2ge  13224  qbtwnre  13225  qbtwnxr  13226  xralrple  13231  xrsupsslem  13333  xrinfmsslem  13334  supxrpnf  13344  icc0  13420  uzsup  13896  expnbnd  14268  expmulnbnd  14271  hashkf  14368  hashdom  14415  iswrdi  14554  rtrclreclem1  15094  rtrclreclem2  15096  rtrclreclem3  15097  01sqrex  15300  resqrex  15301  sqrtneg  15318  abs1m  15387  rexanuz  15397  rexuz3  15400  rexuzre  15404  sqreu  15412  o1lo1  15588  climconst  15594  rlimclim1  15596  climshftlem  15625  rlimo1  15668  lo1add  15678  lo1mul  15679  lo1le  15703  isercoll  15719  serf0  15732  zsum  15769  fsum  15771  fsumcvg3  15780  mertenslem1  15938  ntrivcvgn0  15952  ntrivcvgmullem  15955  zprod  15991  fprod  15995  fprodntriv  15996  dvdsval2  16313  dvds0lem  16324  dvds1lem  16325  dvds2lem  16326  odd2np1lem  16398  odd2np1  16399  opeo  16423  omeo  16424  divalglem9  16459  gcdcllem3  16559  lcmcllem  16654  qredeu  16716  exprmfct  16763  isprm5  16766  odzcllem  16852  reumodprminv  16864  modprm0  16865  nnnn0modprm0  16866  pythagtriplem19  16893  pcprmpw2  16942  pockthi  16967  infpnlem2  16971  vdwlem2  17042  vdwlem10  17050  vdwlem13  17053  ramub1lem1  17086  cshwrepswhash1  17162  imasleval  17595  mreexexlem3d  17702  mreexexlem4d  17703  iscatd  17729  cat1  18154  poslubd  18467  fpwipodrs  18596  ismgmid2  18726  mgmidsssn0  18730  gsumval2a  18743  ismndd  18814  isgrpd2  19023  isgrpd  19025  imasgrp2  19121  mhmmnd  19130  ghmgrp  19132  gaorber  19378  orbsta  19383  cayleyth  19485  pmtrdifel  19550  pmtrdifwrdel  19555  pmtrdifwrdel2  19556  psgnunilem2  19565  psgnunilem3  19566  psgnvalii  19579  pgpfi1  19665  sylow1lem3  19670  sylow1lem5  19672  pgpfi  19675  sylow2alem2  19688  efgredeu  19822  lt6abl  19965  pgpfac1lem3a  20148  pgpfac1lem3  20149  pgpfac1lem5  20151  pgpfaclem1  20153  pgpfaclem3  20155  ablfaclem2  20158  dvdsrmul  20446  dvdsr01  20453  irredrmul  20509  rhmdvdsr  20591  rgspnval  20697  rgspncl  20698  lspf  21073  lspval  21074  lssats2  21099  lspfixed  21230  lspsolvlem  21244  zringlpir  21586  pzriprnglem13  21612  zncyg  21667  cygth  21690  frlmup4  21920  aspval  21991  evlseu  22203  fiinbas  23078  topbas  23098  pptbas  23134  clsval  23163  elcls  23199  neiint  23230  neips  23239  opnneissb  23240  opnssneib  23241  innei  23251  neiptopnei  23258  restbas  23284  neitr  23306  pnfnei  23346  mnfnei  23347  lmconst  23387  iscnp4  23389  cncnpi  23404  cnconst2  23409  cnprest  23415  cnpdis  23419  nrmsep  23483  regsep2  23502  cmpcovf  23517  cmpsub  23526  cmpcld  23528  hauscmplem  23532  conncompid  23557  2ndci  23574  2ndcsb  23575  2ndc1stc  23577  1stcrest  23579  2ndcctbss  23581  2ndcdisj  23582  2ndcomap  23584  2ndcsep  23585  dis2ndc  23586  restlly  23609  islly2  23610  hausllycmp  23620  cldllycmp  23621  lly1stc  23622  dislly  23623  ssref  23638  refref  23639  finlocfin  23646  dissnlocfin  23655  locfindis  23656  llycmpkgen2  23676  cmpkgen  23677  1stckgenlem  23679  elptr  23699  ptbasfi  23707  neitx  23733  ptpjopn  23738  txcnp  23746  ptcnplem  23747  txlly  23762  txnlly  23763  txtube  23766  txcmplem1  23767  tx1stc  23776  txkgen  23778  xkococnlem  23785  txconn  23815  tgqtop  23838  kqreglem1  23867  kqreglem2  23868  kqnrmlem1  23869  kqnrmlem2  23870  reghmph  23919  nrmhmph  23920  fbssfi  23963  opnfbas  23968  isfil2  23982  fsubbas  23993  ssfg  23998  fgss2  24000  fbasrn  24010  filuni  24011  fgtr  24016  ssufl  24044  uffix  24047  elfm2  24074  elfm3  24076  imaelfm  24077  rnelfmlem  24078  rnelfm  24079  fmfnfmlem4  24083  fmfnfm  24084  fmco  24087  ufldom  24088  hausflim  24107  flimcls  24111  hauspwpwf1  24113  flffbas  24121  txflf  24132  fclscf  24151  fclsfnflim  24153  alexsubALTlem4  24176  alexsubALT  24177  tmdgsum2  24222  symgtgp  24232  subgntr  24233  opnsubg  24234  ghmcnp  24241  qustgpopn  24246  tsmsfbas  24254  tsmsxplem1  24279  ustexsym  24342  trust  24355  utoptop  24360  restutop  24363  restutopopn  24364  ustuqtop4  24370  utopsnneiplem  24373  iducn  24408  fmucnd  24417  cfilufg  24418  trcfilu  24419  neipcfilu  24421  imasdsf1olem  24499  blssps  24550  blss  24551  blssexps  24552  blssex  24553  ssblex  24554  blin2  24555  neibl  24627  blcld  24631  metss2  24638  stdbdmopn  24644  met1stc  24647  met2ndci  24648  metrest  24650  prdsxmslem2  24655  metcnp3  24666  metustexhalf  24682  metustfbas  24683  cfilucfil  24685  restmetu  24696  dscopn  24699  ngptgp  24762  nlmvscnlem1  24812  tgioo  24922  tgqioo  24926  xrsmopn  24939  zcld  24940  recld2  24941  zdis  24943  icccmplem1  24949  icccmplem2  24950  xmetdcn2  24964  addcnlem  24991  xrhmeo  25074  cnheibor  25083  cnllycmp  25084  lebnumlem3  25091  lebnum  25092  xlebnum  25093  lebnumii  25094  elpi1i  25174  ipcnlem1  25373  lmnn  25391  iscfil3  25401  cfilres  25424  flimcfil  25442  bcthlem4  25455  bcthlem5  25456  minveclem4c  25553  minveclem2  25554  minveclem3b  25556  minveclem3  25557  minveclem4  25560  minveclem6  25562  ivthlem2  25580  ivth  25582  ivthle  25584  ivthle2  25585  elovolmr  25604  ovolunlem1  25625  ovoliunlem2  25631  ovolicc1  25644  iundisj  25676  iunmbl2  25685  dyadmbllem  25727  volivth  25735  mbflimsup  25794  i1faddlem  25821  i1fmullem  25822  itg2lr  25858  itg2monolem1  25878  limcnlp  26006  ellimc3  26007  limcflf  26009  limciun  26022  rollelem  26117  c1lip1  26125  lhop1lem  26141  ply1divex  26263  ig1peu  26301  elply2  26322  coeeq  26353  plydivlem3  26425  plydivlem4  26426  elqaalem3  26451  qaa  26453  iaa  26455  aareccl  26456  aannenlem2  26459  aalioulem2  26463  aalioulem3  26464  aalioulem5  26466  aalioulem6  26467  aaliou  26468  aaliou2  26470  aaliou3lem8  26475  ulmshftlem  26518  reeff1o  26576  pilem2  26581  pilem3  26582  efif1olem2  26674  efopn  26789  cxpcn3lem  26878  cxpeq  26888  dcubic2  26975  quart  26992  xrlimcnp  27099  ftalem5  27207  ftalem7  27209  sgmnncl  27277  dvdsppwf1o  27316  musum  27321  perfect  27361  dchrptlem1  27394  dchrptlem2  27395  dchrpt  27397  bpos1lem  27412  lgsqrlem4  27479  lgsdchrval  27484  2sqblem  27561  dchrisumlem3  27621  chpdifbndlem2  27684  pntrsumbnd2  27697  pntpbnd1  27716  pntpbnd2  27717  pntpbnd  27718  pntibndlem2  27721  pntibndlem3  27722  pntleme  27738  pntlem3  27739  elno2  27784  ltsval2  27786  noreson  27790  ltsres  27792  noseponlem  27794  nolesgn2o  27801  nogesgn1o  27803  nodense  27822  nosupfv  27836  nosupres  27837  nosupbnd1lem3  27840  nosupbnd1lem5  27842  nosupbnd2lem1  27845  noinffv  27851  noinfres  27852  noinfbnd1lem3  27855  noinfbnd1lem5  27857  noinfbnd2lem1  27860  noetasuplem4  27866  noetainflem4  27870  noetalem2  27872  cuteq0  27974  cuteq1  27976  oldlim  28046  bdayiun  28074  cofcutrtime  28086  cofss  28089  coiniss  28090  cutlt  28091  cutmax  28093  cutmin  28094  negsex  28202  negsfo  28212  norecdiv  28349  divs1  28363  precsexlem11  28376  precsex  28377  recsex  28378  elons2d  28418  oncutlt  28423  n0on  28495  bdayn0sf1o  28529  dfnns2  28531  zsoring  28568  pw2recs  28597  halfcut  28617  0reno  28655  1reno  28656  readdscl  28658  axtgcont  28704  tgcgrxfr  28753  legid  28822  btwnleg  28823  leg0  28827  tghilberti1  28872  colline  28885  mirreu3  28893  isperp2  28954  colperpex  28973  lnopp2hpgb  29004  hpgerlem  29006  brbtwn  29190  brcgr  29191  brbtwn2  29196  axpasch  29232  axlowdimlem14  29246  axlowdim2  29251  axcontlem2  29256  axcontlem4  29258  axcontlem8  29262  axcontlem10  29264  axcontlem12  29266  fusgrn0degnn0  29790  friendshipgt3  30690  lpni  30773  isgrpoi  30791  vacn  30987  smcnlem  30990  nmosetn0  31058  nmoolb  31064  nmobndi  31068  nmoo0  31084  nmlno0lem  31086  isblo3i  31094  blo3i  31095  blocnilem  31097  ubthlem1  31163  minvecolem2  31168  minvecolem3  31169  minvecolem4c  31172  minvecolem4  31173  minvecolem5  31174  minvecolem6  31175  norm1exi  31543  occl  31597  spanval  31626  spancl  31629  shsval2i  31680  ococin  31701  pjoml6i  31882  nmopsetn0  32158  nmfnsetn0  32171  nmoplb  32200  nmfnlb  32217  nmop0  32279  nmfn0  32280  nmlnop0iALT  32288  nmopun  32307  nmcexi  32319  lnconi  32326  lnopcnbd  32329  lnfncnbd  32350  riesz3i  32355  riesz1  32358  cnlnadjlem2  32361  cnlnadjlem8  32367  cnlnadjlem9  32368  adjbd1o  32378  branmfn  32398  opsqrlem1  32433  pjnmopi  32441  strlem1  32543  stri  32550  hstri  32558  cvcon3  32577  cvnbtwn  32579  superpos  32647  shatomici  32651  atcvat4i  32690  mdsymlem2  32697  cdj1i  32726  cdj3i  32734  rexunirn  32779  foresf1o  32791  iundisjf  32875  aciunf1lem  32948  fnpreimac  32956  fgreu  32957  fcnvgreu  32958  xrge0infss  33046  ssnnssfz  33073  iundisjfi  33082  indf1ofs  33127  xreceu  33182  rexdiv  33186  isarchi3  33448  archirngz  33450  archiabllem2a  33455  0nellinds  33628  qtophaus  34171  reff  34174  locfinreflem  34175  cmpcref  34185  dispcmp  34194  tpr2rico  34247  pnfneige0  34286  qqhucn  34327  rrhre  34356  esumcst  34398  esumpcvgval  34413  dmsigagen  34479  rossros  34515  dya2icoseg  34612  dya2iocnrect  34616  dya2iocuni  34618  eulerpartlemgvv  34711  dstfrvunirn  34810  ballotlem4  34834  ballotlemic  34842  ballotlemrc  34866  signsw0g  34888  signswmnd  34889  prodfzo03  34935  tgoldbachgt  34995  onvf1odlem4  35523  loop1cycl  35562  umgr2cycllem  35565  umgr2cycl  35566  subfacp1lem3  35607  erdsze2lem2  35629  cnpconn  35655  txpconn  35657  ptpconn  35658  indispconn  35659  connpconn  35660  cvxpconn  35667  cnllysconn  35670  cvmsss2  35699  cvmcov2  35700  cvmopnlem  35703  cvmliftlem14  35722  cvmliftlem15  35723  cvmlift2lem11  35738  cvmlift2lem12  35739  cvmlift2lem13  35740  cvmlift3lem2  35745  cvmlift3lem6  35749  cvmlift3lem9  35752  mthmi  36002  r1peuqusdeg1  36068  br8  36181  br6  36182  br4  36183  dfon2lem9  36214  wzel  36247  wsuclem  36248  wsuclb  36251  imagesset  36378  fvtransport  36457  brcolinear  36484  brsegle  36533  seglerflx  36537  seglemin  36538  btwnsegle  36542  fvray  36566  fvline  36569  hilbert1.1  36579  elhf2  36600  0hf  36602  nn0prpwlem  36756  nn0prpw  36757  fness  36783  fneref  36784  fnessref  36791  refssfne  36792  neibastop2lem  36794  fnemeet1  36800  tailfb  36811  filnetlem4  36815  limsucncmpi  36879  ttctr  36927  dfttc2g  36940  taupilemrplb  37886  qdiff  37893  relowlssretop  37931  rdgellim  37944  matunitlindflem2  38190  ptrecube  38193  poimirlem4  38197  poimirlem17  38210  poimirlem20  38213  poimirlem23  38216  poimirlem24  38217  poimirlem26  38219  poimirlem27  38220  poimirlem29  38222  poimirlem32  38225  heicant  38228  mblfinlem1  38230  mblfinlem2  38231  mblfinlem3  38232  mblfinlem4  38233  ismblfin  38234  volsupnfl  38238  itg2addnclem  38244  itg2addnclem3  38246  itg2addnc  38247  ftc1anclem5  38270  unirep  38287  cover2  38288  indexa  38306  frinfm  38308  sdclem1  38316  fdc  38318  incsequz  38321  caushft  38334  istotbnd3  38344  0totbnd  38346  sstotbnd2  38347  sstotbnd  38348  sstotbnd3  38349  isbnd3  38357  ssbnd  38361  equivbnd  38363  prdsbnd  38366  prdstotbnd  38367  cntotbnd  38369  heibor1lem  38382  heiborlem1  38384  heiborlem3  38386  heiborlem6  38389  heiborlem8  38391  bfplem2  38396  rrncmslem  38405  iccbnd  38413  opidonOLD  38425  exidres  38451  isrngod  38471  isgrpda  38528  isdrngo2  38531  igenval  38634  igenidl  38636  prtlem10  39563  lshpnel2N  39683  lsmsat  39706  lssatomic  39709  lcvnbtwn  39723  lfl1  39768  eqlkr  39797  lshpkrlem1  39808  lshpkrex  39816  cvrcon3b  39975  cvrat4  40141  3dim3  40167  ps-2  40176  llni  40206  llnle  40216  lplni  40230  lplnle  40238  lplnexllnN  40262  lvoli  40273  lnatexN  40477  elpaddn0  40498  pclfinN  40598  lhprelat3N  40738  4atexlemex2  40769  4atex  40774  4atex2-0aOLDN  40776  4atex2-0cOLDN  40778  lautcvr  40790  cdleme0ex1N  40921  cdleme50rnlem  41242  cdleme50ex  41257  cdlemg1cex  41286  cdlemkid5  41633  cdlemk  41672  tendoex  41673  cdleml5N  41678  cdlemm10N  41816  dih1dimatlem0  42026  dihjat1lem  42126  dvh3dim2  42146  dvh3dim3N  42147  dochkr1  42176  dochkr1OLDN  42177  lcfrvalsnN  42239  lcfrlem27  42267  lcfrlem37  42277  lcfr  42283  mapd1o  42346  mapdpglem23  42392  hdmap11lem2  42540  primrootsunit1  42788  zdivgd  43022  resubeu  43062  fidomncyc  43229  nacsfix  43369  mzpcompact2lem  43408  eldioph  43415  diophrw  43416  diophin  43429  rexrabdioph  43447  rexzrexnn0  43457  eldioph4b  43464  rencldnfilem  43473  irrapxlem5  43479  irrapxlem6  43480  pell1234qrdich  43514  pell14qrdich  43522  infmrgelbi  43531  pellqrex  43532  pellfundre  43534  pellfundlb  43537  rmxynorm  43571  congrep  43626  acongrep  43633  jm2.27  43661  fnwe2lem2  43704  islssfgi  43725  hbtlem2  43777  hbtlem4  43779  hbtlem5  43781  dgraaub  43801  mpaaeu  43803  aaitgo  43815  unielss  43871  onexgt  43893  onexomgt  43894  onexlimgt  43896  onexoegt  43897  oaordnr  43949  omnord1  43958  oenord1  43969  oaomoencom  43970  oenass  43972  tfsconcatfv2  43993  tfsconcatrn  43995  tfsconcatb0  43997  ofoafo  44009  naddcnffo  44017  oaun3lem1  44027  naddwordnexlem4  44054  sucomisnotcard  44196  clsk1independent  44698  0elaxnul  45618  pwclaxpow  45619  prclaxpr  45620  uniclaxun  45621  omssaxinf2  45623  wfac8prim  45637  restuni3  45762  iinssd  45775  founiiun  45823  wessf1ornlem  45829  founiiun0  45834  unirnmap  45850  dstregt0  45927  uzfissfz  45968  rpgtrecnn  46021  rexabslelem  46058  infrnmptle  46063  infxrunb3rnmpt  46068  infxrpnf  46086  supminfxr  46104  rexanuz2nf  46132  iooiinicc  46184  iooiinioc  46198  uzubioo  46207  climsuse  46250  islptre  46261  limsuppnfdlem  46341  climinf3  46356  limsupmnfuzlem  46366  limsupre3lem  46372  limsupre3uzlem  46375  0cnv  46382  liminfreuzlem  46442  cnrefiisplem  46469  icccncfext  46527  cncficcgt0  46528  dvbdfbdioo  46570  ioodvbdlimc1lem1  46571  ioodvbdlimc1lem2  46572  ioodvbdlimc2lem  46574  stoweidlem9  46649  stoweidlem14  46654  stoweidlem18  46658  stoweidlem21  46661  stoweidlem29  46669  stoweidlem34  46674  stoweidlem35  46675  stoweidlem39  46679  stoweidlem41  46681  stoweidlem45  46685  stoweidlem52  46692  stoweidlem55  46695  stoweidlem57  46697  stoweidlem60  46700  stirlinglem5  46718  stirlinglem13  46726  stirlinglem14  46727  fourierdlem16  46763  fourierdlem20  46767  fourierdlem21  46768  fourierdlem22  46769  fourierdlem25  46772  fourierdlem31  46778  fourierdlem39  46786  fourierdlem41  46788  fourierdlem42  46789  fourierdlem47  46793  fourierdlem48  46794  fourierdlem51  46797  fourierdlem63  46809  fourierdlem64  46810  fourierdlem65  46811  fourierdlem77  46823  fourierdlem81  46827  fourierdlem83  46829  fourierdlem103  46849  fourierdlem104  46850  elaa2lem  46873  etransclem47  46921  qndenserrnbl  46935  ioorrnopnlem  46944  ioorrnopnxrlem  46946  intsaluni  46969  salgencntex  46983  subsaliuncllem  46997  sge0resplit  47046  sge0seq  47086  sge0reuz  47087  nnfoctbdjlem  47095  meaiininclem  47126  hoicvrrex  47196  ovnlecvr  47198  ovnlerp  47202  hoidmv1lelem2  47232  hoidmvlelem2  47236  hoidmvlelem3  47237  ovnhoilem1  47241  ovnlecvr2  47250  hoiqssbl  47265  ovolval4lem2  47290  ovolval5lem2  47293  ovnovollem1  47296  ovnovollem2  47297  iinhoiicclem  47313  smfinflem  47457  smflimsuplem7  47466  nthrucw  47528  sprsymrelfolem2  48165  perfectALTV  48411  9gbo  48462  11gbo  48463  nnsum3primes4  48476  nnsum3primesprm  48478  ssnn0ssfz  49048  lincsumcl  49130  lincscmcl  49131  zlmodzxzldep  49203  ldepsnlinc  49207  line2ylem  49450  line2xlem  49452  sepfsepc  49625  lubsscl  49657  glbsscl  49658  nelsubc3lem  49767  cnelsubclem  50300  aacllem  50509