Theorem rspcev 3576

Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2178, ax-11 2194, ax-12 2213. (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 487	. . 3 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓))
4	1, 3	rspcedv 3569	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝜓 → ∃𝑥 ∈ 𝐵 𝜑))
5	4	imp 412	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087

This theorem is used by:  rspcedvdw  3579  rspceaimv  3582  rspc2ev  3589  rspc3ev  3593  rspceeqv  3599  reu6i  3686  rspesbca  3828  eliuni  4957  iuneqconst  4963  brralrspcev  5165  wefrc  5649  wereu2  5652  xpdifid  6160  xpdifcnvepel  6161  frpomin  6338  onfr  6397  onelssex  6407  ordunidif  6408  eliman0  6916  dffv2  6974  elrnrexdm  7083  eldmrexrn  7085  elabrex  7240  elabrexg  7241  f1elima  7261  fliftfun  7314  fliftval  7318  f1oiso2  7354  sorpssuni  7734  sorpssint  7735  onssmin  7792  onminex  7802  fimaproj  8134  frxp3  8150  poseq  8157  tfrlem12  8379  seqomlem2  8443  oawordeulem  8544  oaass  8551  odi  8569  omass  8570  omeulem1  8572  oen0  8577  oelim2  8586  oeeulem  8592  nnawordex  8628  nnaordex2  8630  eldifsucnn  8655  cofon1  8663  cofon2  8664  naddcllem  8667  naddunif  8685  boxcutc  8951  0fi  9052  snfi  9053  rexdif1en  9158  findcard  9161  nnfi  9165  pssnn  9166  unfi  9168  onfin  9212  dif1ennnALT  9250  frfi  9258  fisupg  9261  nnsdomg  9272  pwfir  9289  prfi  9296  fissuni  9327  fipreima  9328  finsschain  9329  indexfi  9330  marypha1lem  9406  eqsup  9429  supmax  9441  fisup2g  9442  fisupcl  9443  supisoex  9448  infmin  9469  fiinfg  9474  fiinf2g  9475  wofib  9520  wemaplem2  9522  card2inf  9530  brwdom2  9548  cnfcom3clem  9687  ssttrcl  9697  ttrcltr  9698  trcl  9710  frmin  9734  r1ordg  9763  r1pwss  9769  tz9.12lem3  9774  tz9.12  9775  r1elwf  9781  tcrank  9869  scottex  9875  scottexOLD  9876  scott0b  9879  scott0OLD  9880  isnumi  9954  onsdom  10004  ondomen  10043  infpwfien  10068  cardaleph  10095  infenaleph  10097  alephfplem4  10113  alephfp2  10115  dfac2b  10136  ackbij1lem18  10241  ackbij1  10242  cflem  10250  cflecard  10257  cfsuc  10262  cfflb  10264  cofsmo  10274  coftr  10278  fin23lem7  10321  fin23lem11  10322  enfin2i  10326  fin23lem26  10330  isf32lem5  10362  isf34lem4  10382  isfin1-3  10391  fin1a2lem7  10411  axdc3lem4  10458  ttukeylem7  10520  iunfo  10550  ficard  10576  pwcfsdom  10595  fpwwe2lem11  10653  wunex  10751  eltsk2g  10763  grur1  10832  axgroth6  10840  inaprc  10848  nqereu  10941  archnq  10992  genpnmax  11019  ltexpri  11055  prlem936  11059  recexpr  11063  supexpr  11066  negexsr  11114  recexsrlem  11115  recexsr  11119  supsrlem  11123  axrnegex  11174  axrrecex  11175  axpre-sup  11181  1re  11235  dedekind  11400  dedekindle  11401  cnegex  11418  cnegex2  11419  recex  11873  receu  11886  fiminre2  12190  cju  12241  nn2ge  12290  nominpos  12508  zdiv  12694  btwnz  12727  uzwo  12963  ublbneg  12985  lbzbi  12988  zsupss  12989  uzsupss  12992  rpnnen1lem1  13031  rpnnen1lem3  13032  rpnnen1lem4  13033  rpnnen1lem5  13034  z2ge  13253  qbtwnre  13254  qbtwnxr  13255  xralrple  13260  xrsupsslem  13362  xrinfmsslem  13363  supxrpnf  13373  icc0  13449  uzsup  13927  expnbnd  14299  expmulnbnd  14302  hashkf  14399  hashdom  14446  iswrdi  14585  rtrclreclem1  15133  rtrclreclem2  15135  rtrclreclem3  15136  01sqrex  15339  resqrex  15340  sqrtneg  15357  abs1m  15426  rexanuz  15436  rexuz3  15439  rexuzre  15443  sqreu  15451  o1lo1  15627  climconst  15633  rlimclim1  15635  climshftlem  15664  rlimo1  15707  lo1add  15717  lo1mul  15718  lo1le  15742  isercoll  15758  serf0  15771  zsum  15807  fsum  15809  fsumcvg3  15818  mertenslem1  15976  ntrivcvgn0  15990  ntrivcvgmullem  15993  zprod  16027  fprod  16031  fprodntriv  16032  dvdsval2  16348  dvds0lem  16359  dvds1lem  16360  dvds2lem  16361  odd2np1lem  16433  odd2np1  16434  opeo  16458  omeo  16459  divalglem9  16494  gcdcllem3  16594  lcmcllem  16689  qredeu  16751  exprmfct  16798  isprm5  16801  odzcllem  16887  reumodprminv  16899  modprm0  16900  nnnn0modprm0  16901  pythagtriplem19  16928  pcprmpw2  16977  pockthi  17002  infpnlem2  17006  vdwlem2  17077  vdwlem10  17085  vdwlem13  17088  ramub1lem1  17121  cshwrepswhash1  17197  imasleval  17630  mreexexlem3d  17737  mreexexlem4d  17738  iscatd  17764  cat1  18189  poslubd  18502  fpwipodrs  18631  ismgmid2  18765  mgmidsssn0  18769  mgmidpfod  18773  gsumval2a  18790  ismndd  18862  isgrpd2  19083  isgrpd  19085  imasgrp2  19181  mhmmnd  19190  ghmgrp  19192  gaorber  19438  orbsta  19443  cayleyth  19545  pmtrdifel  19610  pmtrdifwrdel  19615  pmtrdifwrdel2  19616  psgnunilem2  19625  psgnunilem3  19626  psgnvalii  19639  pgpfi1  19725  sylow1lem3  19730  sylow1lem5  19732  pgpfi  19735  sylow2alem2  19748  efgredeu  19882  lt6abl  20025  pgpfac1lem3a  20208  pgpfac1lem3  20209  pgpfac1lem5  20211  pgpfaclem1  20213  pgpfaclem3  20215  ablfaclem2  20218  dvdsrmul  20508  dvdsr01  20515  irredrmul  20571  rhmdvdsr  20671  rgspnval  20777  rgspncl  20778  lspf  21161  lspval  21162  lssats2  21187  lspfixed  21318  lspsolvlem  21332  zringlpir  21683  pzriprnglem13  21709  zncyg  21764  cygth  21787  frlmup4  22017  aspval  22090  evlseu  22302  matunitlindflem2  22905  fiinbas  23180  topbas  23200  pptbas  23236  clsval  23265  elcls  23301  neiint  23332  neips  23341  opnneissb  23342  opnssneib  23343  innei  23353  neiptopnei  23360  restbas  23386  neitr  23408  pnfnei  23448  mnfnei  23449  lmconst  23489  iscnp4  23491  cncnpi  23506  cnconst2  23511  cnprest  23517  cnpdis  23521  nrmsep  23585  regsep2  23604  cmpcovf  23619  cmpsub  23628  cmpcld  23630  hauscmplem  23634  conncompid  23659  2ndci  23676  2ndcsb  23677  2ndc1stc  23679  1stcrest  23681  2ndcctbss  23684  2ndcdisj  23685  2ndcomap  23687  2ndcsep  23688  dis2ndc  23689  restlly  23712  islly2  23713  hausllycmp  23723  cldllycmp  23724  lly1stc  23725  dislly  23726  ssref  23741  refref  23742  finlocfin  23749  dissnlocfin  23758  locfindis  23759  llycmpkgen2  23779  cmpkgen  23780  1stckgenlem  23782  elptr  23802  ptbasfi  23810  neitx  23836  ptpjopn  23841  txcnp  23849  ptcnplem  23850  txlly  23865  txnlly  23866  txtube  23869  txcmplem1  23870  tx1stc  23879  txkgen  23881  xkococnlem  23888  txconn  23918  tgqtop  23941  kqreglem1  23970  kqreglem2  23971  kqnrmlem1  23972  kqnrmlem2  23973  reghmph  24022  nrmhmph  24023  fbssfi  24066  opnfbas  24071  isfil2  24085  fsubbas  24096  ssfg  24101  fgss2  24103  fbasrn  24113  filuni  24114  fgtr  24119  ssufl  24147  uffix  24150  elfm2  24177  elfm3  24179  imaelfm  24180  rnelfmlem  24181  rnelfm  24182  fmfnfmlem4  24186  fmfnfm  24187  fmco  24190  ufldom  24191  hausflim  24210  flimcls  24214  hauspwpwf1  24216  flffbas  24224  txflf  24235  fclscf  24254  fclsfnflim  24256  alexsubALTlem4  24279  alexsubALT  24280  tmdgsum2  24325  symgtgp  24335  subgntr  24336  opnsubg  24337  ghmcnp  24344  qustgpopn  24349  tsmsfbas  24357  tsmsxplem1  24382  ustexsym  24445  trust  24458  utoptop  24463  restutop  24466  restutopopn  24467  ustuqtop4  24473  utopsnneiplem  24476  iducn  24511  fmucnd  24520  cfilufg  24521  trcfilu  24522  neipcfilu  24524  imasdsf1olem  24602  blssps  24653  blss  24654  blssexps  24655  blssex  24656  ssblex  24657  blin2  24658  neibl  24730  blcld  24734  metss2  24741  stdbdmopn  24747  met1stc  24750  met2ndci  24751  metrest  24753  prdsxmslem2  24758  metcnp3  24769  metustexhalf  24785  metustfbas  24786  cfilucfil  24788  restmetu  24799  dscopn  24802  ngptgp  24865  nlmvscnlem1  24915  tgioo  25025  tgqioo  25029  xrsmopn  25042  zcld  25043  recld2  25044  zdis  25046  icccmplem1  25052  icccmplem2  25053  xmetdcn2  25067  addcnlem  25094  xrhmeo  25177  cnheibor  25186  cnllycmp  25187  lebnumlem3  25194  lebnum  25195  xlebnum  25196  lebnumii  25197  elpi1i  25277  ipcnlem1  25476  lmnn  25494  iscfil3  25504  cfilres  25527  flimcfil  25545  bcthlem4  25558  bcthlem5  25559  minveclem4c  25656  minveclem2  25657  minveclem3b  25659  minveclem3  25660  minveclem4  25663  minveclem6  25665  ivthlem2  25683  ivth  25685  ivthle  25687  ivthle2  25688  elovolmr  25707  ovolunlem1  25728  ovoliunlem2  25734  ovolicc1  25747  iundisj  25779  iunmbl2  25788  dyadmbllem  25830  volivth  25838  mbflimsup  25897  i1faddlem  25924  i1fmullem  25925  itg2lr  25961  itg2monolem1  25981  limcnlp  26108  ellimc3  26109  limcflf  26111  limciun  26124  rollelem  26219  c1lip1  26227  lhop1lem  26243  ply1divex  26365  ig1peu  26403  elply2  26424  coeeq  26456  plydivlem3  26528  plydivlem4  26529  elqaalem3  26556  qaa  26559  iaaOLD  26564  aareccl  26565  aannenlem2  26568  aalioulem2  26572  aalioulem3  26573  aalioulem5  26575  aalioulem6  26576  aaliou  26577  aaliou2  26579  aaliou3lem8  26584  ulmshftlem  26628  reeff1o  26686  pilem2  26691  pilem3  26692  efif1olem2  26783  efopn  26898  cxpcn3lem  26987  cxpeq  26997  dcubic2  27084  quart  27101  xrlimcnp  27208  ftalem5  27316  ftalem7  27318  sgmnncl  27386  dvdsppwf1o  27425  musum  27430  perfect  27470  dchrptlem1  27503  dchrptlem2  27504  dchrpt  27506  bpos1lem  27521  lgsqrlem4  27588  lgsdchrval  27593  2sqblem  27670  dchrisumlem3  27730  chpdifbndlem2  27793  pntrsumbnd2  27806  pntpbnd1  27825  pntpbnd2  27826  pntpbnd  27827  pntibndlem2  27830  pntibndlem3  27831  pntleme  27847  pntlem3  27848  elno2  27893  ltsval2  27895  noreson  27899  ltsres  27901  noseponlem  27903  nolesgn2o  27910  nogesgn1o  27912  nodense  27931  nosupfv  27945  nosupres  27946  nosupbnd1lem3  27949  nosupbnd1lem5  27951  nosupbnd2lem1  27954  noinffv  27960  noinfres  27961  noinfbnd1lem3  27964  noinfbnd1lem5  27966  noinfbnd2lem1  27969  noetasuplem4  27975  noetainflem4  27979  noetalem2  27981  cuteq0  28083  cuteq1  28085  oldlim  28155  bdayiun  28183  cofcutrtime  28195  cofss  28198  coiniss  28199  cutlt  28200  cutmax  28202  cutmin  28203  negsex  28311  negsfo  28321  norecdiv  28458  divs1  28472  precsexlem11  28485  precsex  28486  recsex  28487  elons2d  28527  oncutlt  28532  n0on  28604  bdayn0sf1o  28638  dfnns2  28640  zsoring  28677  pw2recs  28706  halfcut  28726  0reno  28764  1reno  28765  readdscl  28767  axtgcont  28813  tgcgrxfr  28863  legid  28932  btwnleg  28933  leg0  28937  tghilberti1  28987  colline  29000  mirreu3  29008  isperp2  29072  colperpex  29091  lnopp2hpgb  29123  hpgerlem  29125  brbtwn  29359  brcgr  29360  brbtwn2  29365  axpasch  29401  axlowdimlem14  29415  axlowdim2  29420  axcontlem2  29425  axcontlem4  29427  axcontlem8  29431  axcontlem10  29433  axcontlem12  29435  fusgrn0degnn0  29962  loop1cycl  30626  umgr2cycllem  30628  umgr2cycl  30629  friendshipgt3  30881  lpni  30964  isgrpoi  30982  vacn  31178  smcnlem  31181  nmosetn0  31249  nmoolb  31255  nmobndi  31259  nmoo0  31275  nmlno0lem  31277  isblo3i  31285  blo3i  31286  blocnilem  31288  ubthlem1  31354  minvecolem2  31359  minvecolem3  31360  minvecolem4c  31363  minvecolem4  31364  minvecolem5  31365  minvecolem6  31366  norm1exi  31734  occl  31788  spanval  31817  spancl  31820  shsval2i  31871  ococin  31892  pjoml6i  32073  nmopsetn0  32349  nmfnsetn0  32362  nmoplb  32391  nmfnlb  32408  nmop0  32470  nmfn0  32471  nmlnop0iALT  32479  nmopun  32498  nmcexi  32510  lnconi  32517  lnopcnbd  32520  lnfncnbd  32541  riesz3i  32546  riesz1  32549  cnlnadjlem2  32552  cnlnadjlem8  32558  cnlnadjlem9  32559  adjbd1o  32569  branmfn  32589  opsqrlem1  32624  pjnmopi  32632  strlem1  32734  stri  32741  hstri  32749  cvcon3  32768  cvnbtwn  32770  superpos  32838  shatomici  32842  atcvat4i  32881  mdsymlem2  32888  cdj1i  32917  cdj3i  32925  rexunirn  32970  foresf1o  32982  iundisjf  33065  aciunf1lem  33138  fnpreimac  33146  fgreu  33147  fcnvgreu  33148  xrge0infss  33234  ssnnssfz  33261  iundisjfi  33270  indf1ofs  33315  xreceu  33370  rexdiv  33374  isarchi3  33630  archirngz  33632  archiabllem2a  33637  0nellinds  33808  qtophaus  34349  reff  34352  locfinreflem  34353  cmpcref  34363  dispcmp  34372  tpr2rico  34425  pnfneige0  34464  qqhucn  34505  rrhre  34534  esumcst  34576  esumpcvgval  34591  dmsigagen  34658  rossros  34694  dya2icoseg  34791  dya2iocnrect  34795  dya2iocuni  34797  eulerpartlemgvv  34890  dstfrvunirn  34989  ballotlem4  35013  ballotlemic  35021  ballotlemrc  35045  signsw0g  35067  signswmnd  35068  prodfzo03  35114  tgoldbachgt  35174  onvf1odlem4  35706  subfacp1lem3  35764  erdsze2lem2  35786  cnpconn  35812  txpconn  35814  ptpconn  35815  indispconn  35816  connpconn  35817  cvxpconn  35824  cnllysconn  35827  cvmsss2  35856  cvmcov2  35857  cvmopnlem  35860  cvmliftlem14  35879  cvmliftlem15  35880  cvmlift2lem11  35895  cvmlift2lem12  35896  cvmlift2lem13  35897  cvmlift3lem2  35902  cvmlift3lem6  35906  cvmlift3lem9  35909  mthmi  36159  r1peuqusdeg1  36225  br8  36338  br6  36339  br4  36340  dfon2lem9  36371  wzel  36404  wsuclem  36405  wsuclb  36408  imagesset  36535  fvtransport  36615  brcolinear  36642  brsegle  36691  seglerflx  36695  seglemin  36696  btwnsegle  36700  fvray  36724  fvline  36727  hilbert1.1  36737  elhf2  36758  0hf  36760  nn0prpwlem  36944  nn0prpw  36945  fness  36971  fneref  36972  fnessref  36979  refssfne  36980  neibastop2lem  36982  fnemeet1  36988  tailfb  36999  filnetlem4  37003  limsucncmpi  37067  ttctr  37115  dfttc2g  37128  taupilemrplb  38075  qdiff  38082  relowlssretop  38120  rdgellim  38133  ptrecube  38372  poimirlem4  38376  poimirlem17  38389  poimirlem20  38392  poimirlem23  38395  poimirlem24  38396  poimirlem26  38398  poimirlem27  38399  poimirlem29  38401  poimirlem32  38404  heicant  38407  mblfinlem1  38409  mblfinlem2  38410  mblfinlem3  38411  mblfinlem4  38412  ismblfin  38413  volsupnfl  38417  itg2addnclem  38423  itg2addnclem3  38425  itg2addnc  38426  ftc1anclem5  38449  unirep  38467  cover2  38468  indexa  38486  frinfm  38488  sdclem1  38496  fdc  38498  incsequz  38501  caushft  38514  istotbnd3  38524  0totbnd  38526  sstotbnd2  38527  sstotbnd  38528  sstotbnd3  38529  isbnd3  38537  ssbnd  38541  equivbnd  38543  prdsbnd  38546  prdstotbnd  38547  cntotbnd  38549  heibor1lem  38562  heiborlem1  38564  heiborlem3  38566  heiborlem6  38569  heiborlem8  38571  bfplem2  38576  rrncmslem  38585  iccbnd  38593  opidonOLD  38605  exidres  38631  isrngod  38651  isgrpda  38708  isdrngo2  38711  igenval  38814  igenidl  38816  prtlem10  39741  lshpnel2N  39861  lsmsat  39884  lssatomic  39887  lcvnbtwn  39901  lfl1  39946  eqlkr  39975  lshpkrlem1  39986  lshpkrex  39994  cvrcon3b  40153  cvrat4  40319  3dim3  40345  ps-2  40354  llni  40384  llnle  40394  lplni  40408  lplnle  40416  lplnexllnN  40440  lvoli  40451  lnatexN  40655  elpaddn0  40676  pclfinN  40776  lhprelat3N  40916  4atexlemex2  40947  4atex  40952  4atex2-0aOLDN  40954  4atex2-0cOLDN  40956  lautcvr  40968  cdleme0ex1N  41099  cdleme50rnlem  41420  cdleme50ex  41435  cdlemg1cex  41464  cdlemkid5  41811  cdlemk  41850  tendoex  41851  cdleml5N  41856  cdlemm10N  41994  dih1dimatlem0  42204  dihjat1lem  42304  dvh3dim2  42324  dvh3dim3N  42325  dochkr1  42354  dochkr1OLDN  42355  lcfrvalsnN  42417  lcfrlem27  42445  lcfrlem37  42455  lcfr  42461  mapd1o  42524  mapdpglem23  42570  hdmap11lem2  42718  primrootsunit1  42966  zdivgd  43215  resubeu  43255  fidomncyc  43420  nacsfix  43560  mzpcompact2lem  43599  eldioph  43606  diophrw  43607  diophin  43620  rexrabdioph  43638  rexzrexnn0  43648  eldioph4b  43655  rencldnfilem  43664  irrapxlem5  43670  irrapxlem6  43671  pell1234qrdich  43705  pell14qrdich  43713  infmrgelbi  43722  pellqrex  43723  pellfundre  43725  pellfundlb  43728  rmxynorm  43762  congrep  43817  acongrep  43824  jm2.27  43852  fnwe2lem2  43895  islssfgi  43916  hbtlem2  43968  hbtlem4  43970  hbtlem5  43972  dgraaub  43992  mpaaeu  43994  aaitgo  44006  unielss  44062  onexgt  44084  onexomgt  44085  onexlimgt  44087  onexoegt  44088  oaordnr  44140  omnord1  44149  oenord1  44160  oaomoencom  44161  oenass  44163  tfsconcatfv2  44184  tfsconcatrn  44186  tfsconcatb0  44188  ofoafo  44200  naddcnffo  44208  oaun3lem1  44218  naddwordnexlem4  44245  sucomisnotcard  44387  clsk1independent  44889  0elaxnul  45809  pwclaxpow  45810  prclaxpr  45811  uniclaxun  45812  omssaxinf2  45814  wfac8prim  45828  restuni3  45953  iinssd  45966  founiiun  46014  wessf1ornlem  46020  founiiun0  46025  unirnmap  46041  dstregt0  46118  uzfissfz  46159  rpgtrecnn  46212  rexabslelem  46249  infrnmptle  46254  infxrunb3rnmpt  46259  infxrpnf  46277  supminfxr  46295  rexanuz2nf  46323  iooiinicc  46375  iooiinioc  46389  uzubioo  46398  climsuse  46441  islptre  46452  limsuppnfdlem  46532  climinf3  46547  limsupmnfuzlem  46557  limsupre3lem  46563  limsupre3uzlem  46566  0cnv  46573  liminfreuzlem  46633  cnrefiisplem  46660  icccncfext  46718  cncficcgt0  46719  dvbdfbdioo  46761  ioodvbdlimc1lem1  46762  ioodvbdlimc1lem2  46763  ioodvbdlimc2lem  46765  stoweidlem9  46840  stoweidlem14  46845  stoweidlem18  46849  stoweidlem21  46852  stoweidlem29  46860  stoweidlem34  46865  stoweidlem35  46866  stoweidlem39  46870  stoweidlem41  46872  stoweidlem45  46876  stoweidlem52  46883  stoweidlem55  46886  stoweidlem57  46888  stoweidlem60  46891  stirlinglem5  46909  stirlinglem13  46917  stirlinglem14  46918  fourierdlem16  46954  fourierdlem20  46958  fourierdlem21  46959  fourierdlem22  46960  fourierdlem25  46963  fourierdlem31  46969  fourierdlem39  46977  fourierdlem41  46979  fourierdlem42  46980  fourierdlem47  46984  fourierdlem48  46985  fourierdlem51  46988  fourierdlem63  47000  fourierdlem64  47001  fourierdlem65  47002  fourierdlem77  47014  fourierdlem81  47018  fourierdlem83  47020  fourierdlem103  47040  fourierdlem104  47041  elaa2lem  47064  etransclem47  47112  qndenserrnbl  47126  ioorrnopnlem  47135  ioorrnopnxrlem  47137  intsaluni  47160  salgencntex  47174  subsaliuncllem  47188  sge0resplit  47237  sge0seq  47277  sge0reuz  47278  nnfoctbdjlem  47286  meaiininclem  47317  hoicvrrex  47387  ovnlecvr  47389  ovnlerp  47393  hoidmv1lelem2  47423  hoidmvlelem2  47427  hoidmvlelem3  47428  ovnhoilem1  47432  ovnlecvr2  47441  hoiqssbl  47456  ovolval4lem2  47481  ovolval5lem2  47484  ovnovollem1  47487  ovnovollem2  47488  iinhoiicclem  47504  smfinflem  47648  smflimsuplem7  47657  sprsymrelfolem2  48396  perfectALTV  48642  9gbo  48693  11gbo  48694  nnsum3primes4  48707  nnsum3primesprm  48709  ssnn0ssfz  49282  lincsumcl  49364  lincscmcl  49365  zlmodzxzldep  49437  ldepsnlinc  49441  line2ylem  49684  line2xlem  49686  sepfsepc  49857  lubsscl  49889  glbsscl  49890  nelsubc3lem  49999  cnelsubclem  50532  aacllem  50775