Theorem rspcev 3585

Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2142, ax-11 2158, ax-12 2178. (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 22	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ 𝐵)
2		rspcv.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	adantl 481	. . 3 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓))
4	1, 3	rspcedv 3578	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝜓 → ∃𝑥 ∈ 𝐵 𝜑))
5	4	imp 406	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054

This theorem is referenced by:  rspcedvdw  3588  rspceb2dv  3589  rspceaimv  3591  rspc2ev  3598  rspc3ev  3602  rspceeqv  3608  reu6i  3696  rspesbca  3841  eliuni  4957  iuneqconst  4963  brralrspcev  5162  wefrc  5625  wereu2  5628  xpdifid  6129  frpomin  6301  onfr  6359  onelssex  6369  ordunidif  6370  eliman0  6880  dffv2  6938  elrnrexdm  7043  eldmrexrn  7045  elabrex  7198  elabrexg  7199  elunirn2OLD  7209  f1elima  7220  fliftfun  7269  fliftval  7273  f1oiso2  7309  sorpssuni  7688  sorpssint  7689  onssmin  7748  onminex  7758  fimaproj  8091  frxp3  8107  poseq  8114  tfrlem12  8334  seqomlem2  8396  oawordeulem  8495  oaass  8502  odi  8520  omass  8521  omeulem1  8523  oen0  8527  oelim2  8536  oeeulem  8542  nnawordex  8578  nnaordex2  8580  eldifsucnn  8605  cofon1  8613  cofon2  8614  naddcllem  8617  naddunif  8634  boxcutc  8891  0fi  8990  snfi  8991  snfiOLD  8992  rexdif1en  9099  rexdif1enOLD  9100  findcard  9104  nnfi  9108  pssnn  9109  unfi  9112  onfin  9156  dif1ennnALT  9198  frfi  9208  fisupg  9211  nnsdomg  9222  nnsdomgOLD  9223  pwfir  9242  prfi  9250  fissuni  9284  fipreima  9285  finsschain  9286  indexfi  9287  marypha1lem  9360  eqsup  9383  supmax  9395  fisup2g  9396  fisupcl  9397  supisoex  9402  infmin  9423  fiinfg  9428  fiinf2g  9429  wofib  9474  wemaplem2  9476  card2inf  9484  brwdom2  9502  cnfcom3clem  9634  ssttrcl  9644  ttrcltr  9645  trcl  9657  frmin  9678  r1ordg  9707  r1pwss  9713  tz9.12lem3  9718  tz9.12  9719  r1elwf  9725  tcrank  9813  scottex  9814  scott0  9815  isnumi  9875  onsdom  9925  ondomen  9966  infpwfien  9991  cardaleph  10018  infenaleph  10020  alephfplem4  10036  alephfp2  10038  dfac2b  10060  ackbij1lem18  10165  ackbij1  10166  cflem  10174  cflemOLD  10175  cflecard  10182  cfsuc  10186  cfflb  10188  cofsmo  10198  coftr  10202  fin23lem7  10245  fin23lem11  10246  enfin2i  10250  fin23lem26  10254  isf32lem5  10286  isf34lem4  10306  isfin1-3  10315  fin1a2lem7  10335  axdc3lem4  10382  ttukeylem7  10444  iunfo  10468  ficard  10494  pwcfsdom  10512  fpwwe2lem11  10570  wunex  10668  eltsk2g  10680  grur1  10749  axgroth6  10757  inaprc  10765  nqereu  10858  archnq  10909  genpnmax  10936  ltexpri  10972  prlem936  10976  recexpr  10980  supexpr  10983  negexsr  11031  recexsrlem  11032  recexsr  11036  supsrlem  11040  axrnegex  11091  axrrecex  11092  axpre-sup  11098  1re  11150  dedekind  11313  dedekindle  11314  cnegex  11331  cnegex2  11332  recex  11786  receu  11799  fiminre2  12107  cju  12158  nn2ge  12189  nominpos  12395  zdiv  12580  btwnz  12613  uzwo  12846  ublbneg  12868  lbzbi  12871  zsupss  12872  uzsupss  12875  rpnnen1lem1  12913  rpnnen1lem3  12914  rpnnen1lem4  12915  rpnnen1lem5  12916  z2ge  13134  qbtwnre  13135  qbtwnxr  13136  xralrple  13141  xrsupsslem  13243  xrinfmsslem  13244  supxrpnf  13254  icc0  13330  uzsup  13801  expnbnd  14173  expmulnbnd  14176  hashkf  14273  hashdom  14320  iswrdi  14458  rtrclreclem1  14999  rtrclreclem2  15001  rtrclreclem3  15002  01sqrex  15191  resqrex  15192  sqrtneg  15209  abs1m  15278  rexanuz  15288  rexuz3  15291  rexuzre  15295  sqreu  15303  o1lo1  15479  climconst  15485  rlimclim1  15487  climshftlem  15516  rlimo1  15559  lo1add  15569  lo1mul  15570  lo1le  15594  isercoll  15610  serf0  15623  zsum  15660  fsum  15662  fsumcvg3  15671  mertenslem1  15826  ntrivcvgn0  15840  ntrivcvgmullem  15843  zprod  15879  fprod  15883  fprodntriv  15884  dvdsval2  16201  dvds0lem  16212  dvds1lem  16213  dvds2lem  16214  odd2np1lem  16286  odd2np1  16287  opeo  16311  omeo  16312  divalglem9  16347  gcdcllem3  16447  lcmcllem  16542  qredeu  16604  exprmfct  16650  isprm5  16653  odzcllem  16739  reumodprminv  16751  modprm0  16752  nnnn0modprm0  16753  pythagtriplem19  16780  pcprmpw2  16829  pockthi  16854  infpnlem2  16858  vdwlem2  16929  vdwlem10  16937  vdwlem13  16940  ramub1lem1  16973  cshwrepswhash1  17049  imasleval  17480  mreexexlem3d  17583  mreexexlem4d  17584  iscatd  17610  cat1  18035  poslubd  18348  fpwipodrs  18475  ismgmid2  18571  mgmidsssn0  18575  gsumval2a  18588  ismndd  18659  isgrpd2  18864  isgrpd  18866  imasgrp2  18963  mhmmnd  18972  ghmgrp  18974  gaorber  19216  orbsta  19221  cayleyth  19321  pmtrdifel  19386  pmtrdifwrdel  19391  pmtrdifwrdel2  19392  psgnunilem2  19401  psgnunilem3  19402  psgnvalii  19415  pgpfi1  19501  sylow1lem3  19506  sylow1lem5  19508  pgpfi  19511  sylow2alem2  19524  efgredeu  19658  lt6abl  19801  pgpfac1lem3a  19984  pgpfac1lem3  19985  pgpfac1lem5  19987  pgpfaclem1  19989  pgpfaclem3  19991  ablfaclem2  19994  dvdsrmul  20249  dvdsr01  20256  irredrmul  20312  rhmdvdsr  20393  rgspnval  20497  rgspncl  20498  lspf  20856  lspval  20857  lssats2  20882  lspfixed  21014  lspsolvlem  21028  zringlpir  21353  pzriprnglem13  21379  zncyg  21434  cygth  21457  frlmup4  21686  aspval  21758  evlseu  21966  fiinbas  22815  topbas  22835  pptbas  22871  clsval  22900  elcls  22936  neiint  22967  neips  22976  opnneissb  22977  opnssneib  22978  innei  22988  neiptopnei  22995  restbas  23021  neitr  23043  pnfnei  23083  mnfnei  23084  lmconst  23124  iscnp4  23126  cncnpi  23141  cnconst2  23146  cnprest  23152  cnpdis  23156  nrmsep  23220  regsep2  23239  cmpcovf  23254  cmpsub  23263  cmpcld  23265  hauscmplem  23269  conncompid  23294  2ndci  23311  2ndcsb  23312  2ndc1stc  23314  1stcrest  23316  2ndcctbss  23318  2ndcdisj  23319  2ndcomap  23321  2ndcsep  23322  dis2ndc  23323  restlly  23346  islly2  23347  hausllycmp  23357  cldllycmp  23358  lly1stc  23359  dislly  23360  ssref  23375  refref  23376  finlocfin  23383  dissnlocfin  23392  locfindis  23393  llycmpkgen2  23413  cmpkgen  23414  1stckgenlem  23416  elptr  23436  ptbasfi  23444  neitx  23470  ptpjopn  23475  txcnp  23483  ptcnplem  23484  txlly  23499  txnlly  23500  txtube  23503  txcmplem1  23504  tx1stc  23513  txkgen  23515  xkococnlem  23522  txconn  23552  tgqtop  23575  kqreglem1  23604  kqreglem2  23605  kqnrmlem1  23606  kqnrmlem2  23607  reghmph  23656  nrmhmph  23657  fbssfi  23700  opnfbas  23705  isfil2  23719  fsubbas  23730  ssfg  23735  fgss2  23737  fbasrn  23747  filuni  23748  fgtr  23753  ssufl  23781  uffix  23784  elfm2  23811  elfm3  23813  imaelfm  23814  rnelfmlem  23815  rnelfm  23816  fmfnfmlem4  23820  fmfnfm  23821  fmco  23824  ufldom  23825  hausflim  23844  flimcls  23848  hauspwpwf1  23850  flffbas  23858  txflf  23869  fclscf  23888  fclsfnflim  23890  alexsubALTlem4  23913  alexsubALT  23914  tmdgsum2  23959  symgtgp  23969  subgntr  23970  opnsubg  23971  ghmcnp  23978  qustgpopn  23983  tsmsfbas  23991  tsmsxplem1  24016  ustexsym  24079  trust  24093  utoptop  24098  restutop  24101  restutopopn  24102  ustuqtop4  24108  utopsnneiplem  24111  iducn  24146  fmucnd  24155  cfilufg  24156  trcfilu  24157  neipcfilu  24159  imasdsf1olem  24237  blssps  24288  blss  24289  blssexps  24290  blssex  24291  ssblex  24292  blin2  24293  neibl  24365  blcld  24369  metss2  24376  stdbdmopn  24382  met1stc  24385  met2ndci  24386  metrest  24388  prdsxmslem2  24393  metcnp3  24404  metustexhalf  24420  metustfbas  24421  cfilucfil  24423  restmetu  24434  dscopn  24437  ngptgp  24500  nlmvscnlem1  24550  tgioo  24660  tgqioo  24664  xrsmopn  24677  zcld  24678  recld2  24679  zdis  24681  icccmplem1  24687  icccmplem2  24688  xmetdcn2  24702  addcnlem  24729  xrhmeo  24820  cnheibor  24830  cnllycmp  24831  lebnumlem3  24838  lebnum  24839  xlebnum  24840  lebnumii  24841  elpi1i  24922  ipcnlem1  25121  lmnn  25139  iscfil3  25149  cfilres  25172  flimcfil  25190  bcthlem4  25203  bcthlem5  25204  minveclem4c  25301  minveclem2  25302  minveclem3b  25304  minveclem3  25305  minveclem4  25308  minveclem6  25310  ivthlem2  25329  ivth  25331  ivthle  25333  ivthle2  25334  elovolmr  25353  ovolunlem1  25374  ovoliunlem2  25380  ovolicc1  25393  iundisj  25425  iunmbl2  25434  dyadmbllem  25476  volivth  25484  mbflimsup  25543  i1faddlem  25570  i1fmullem  25571  itg2lr  25607  itg2monolem1  25627  limcnlp  25755  ellimc3  25756  limcflf  25758  limciun  25771  rollelem  25869  c1lip1  25878  lhop1lem  25894  ply1divex  26018  ig1peu  26056  elply2  26077  coeeq  26108  plydivlem3  26179  plydivlem4  26180  elqaalem3  26205  qaa  26207  iaa  26209  aareccl  26210  aannenlem2  26213  aalioulem2  26217  aalioulem3  26218  aalioulem5  26220  aalioulem6  26221  aaliou  26222  aaliou2  26224  aaliou3lem8  26229  ulmshftlem  26274  reeff1o  26333  pilem2  26338  pilem3  26339  efif1olem2  26428  efopn  26543  cxpcn3lem  26633  cxpeq  26643  dcubic2  26730  quart  26747  xrlimcnp  26854  ftalem5  26963  ftalem7  26965  sgmnncl  27033  dvdsppwf1o  27072  musum  27077  perfect  27118  dchrptlem1  27151  dchrptlem2  27152  dchrpt  27154  bpos1lem  27169  lgsqrlem4  27236  lgsdchrval  27241  2sqblem  27318  dchrisumlem3  27378  chpdifbndlem2  27441  pntrsumbnd2  27454  pntpbnd1  27473  pntpbnd2  27474  pntpbnd  27475  pntibndlem2  27478  pntibndlem3  27479  pntleme  27495  pntlem3  27496  elno2  27542  sltval2  27544  noreson  27548  sltres  27550  noseponlem  27552  nolesgn2o  27559  nogesgn1o  27561  nodense  27580  nosupfv  27594  nosupres  27595  nosupbnd1lem3  27598  nosupbnd1lem5  27600  nosupbnd2lem1  27603  noinffv  27609  noinfres  27610  noinfbnd1lem3  27613  noinfbnd1lem5  27615  noinfbnd2lem1  27618  noetasuplem4  27624  noetainflem4  27628  noetalem2  27630  cuteq0  27720  cuteq1  27722  oldlim  27774  cofcutrtime  27811  cofss  27814  coiniss  27815  cutlt  27816  cutmax  27818  cutmin  27819  negsex  27925  negsfo  27935  norecdiv  28069  divs1  28083  precsexlem11  28095  precsex  28096  recsex  28097  elons2d  28136  onscutlt  28141  n0ons  28204  bdayn0sf1o  28235  dfnns2  28237  pw2recs  28299  halfcut  28309  0reno  28324  readdscl  28326  axtgcont  28372  tgcgrxfr  28421  legid  28490  btwnleg  28491  leg0  28495  tghilberti1  28540  tglnpt2  28544  colline  28552  mirreu3  28557  isperp2  28618  colperpex  28636  lnopp2hpgb  28666  hpgerlem  28668  brbtwn  28802  brcgr  28803  brbtwn2  28808  axpasch  28844  axlowdimlem14  28858  axlowdim2  28863  axcontlem2  28868  axcontlem4  28870  axcontlem8  28874  axcontlem10  28876  axcontlem12  28878  fusgrn0degnn0  29403  friendshipgt3  30300  lpni  30382  isgrpoi  30400  vacn  30596  smcnlem  30599  nmosetn0  30667  nmoolb  30673  nmobndi  30677  nmoo0  30693  nmlno0lem  30695  isblo3i  30703  blo3i  30704  blocnilem  30706  ubthlem1  30772  minvecolem2  30777  minvecolem3  30778  minvecolem4c  30781  minvecolem4  30782  minvecolem5  30783  minvecolem6  30784  norm1exi  31152  occl  31206  spanval  31235  spancl  31238  shsval2i  31289  ococin  31310  pjoml6i  31491  nmopsetn0  31767  nmfnsetn0  31780  nmoplb  31809  nmfnlb  31826  nmop0  31888  nmfn0  31889  nmlnop0iALT  31897  nmopun  31916  nmcexi  31928  lnconi  31935  lnopcnbd  31938  lnfncnbd  31959  riesz3i  31964  riesz1  31967  cnlnadjlem2  31970  cnlnadjlem8  31976  cnlnadjlem9  31977  adjbd1o  31987  branmfn  32007  opsqrlem1  32042  pjnmopi  32050  strlem1  32152  stri  32159  hstri  32167  cvcon3  32186  cvnbtwn  32188  superpos  32256  shatomici  32260  atcvat4i  32299  mdsymlem2  32306  cdj1i  32335  cdj3i  32343  rexunirn  32394  foresf1o  32406  iundisjf  32491  aciunf1lem  32559  fnpreimac  32568  fgreu  32569  fcnvgreu  32570  xrge0infss  32656  ssnnssfz  32683  iundisjfi  32692  indf1ofs  32762  xreceu  32815  rexdiv  32819  isarchi3  33114  archirngz  33116  archiabllem2a  33121  0nellinds  33314  qtophaus  33799  reff  33802  locfinreflem  33803  cmpcref  33813  dispcmp  33822  tpr2rico  33875  pnfneige0  33914  qqhucn  33955  rrhre  33984  esumcst  34026  esumpcvgval  34041  dmsigagen  34107  rossros  34143  dya2icoseg  34241  dya2iocnrect  34245  dya2iocuni  34247  eulerpartlemgvv  34340  dstfrvunirn  34439  ballotlem4  34463  ballotlemic  34471  ballotlem1c  34472  ballotlemrc  34495  signsw0g  34520  signswmnd  34521  prodfzo03  34567  tgoldbachgt  34627  onvf1odlem4  35066  loop1cycl  35097  umgr2cycllem  35100  umgr2cycl  35101  subfacp1lem3  35142  erdsze2lem2  35164  cnpconn  35190  txpconn  35192  ptpconn  35193  indispconn  35194  connpconn  35195  cvxpconn  35202  cnllysconn  35205  cvmsss2  35234  cvmcov2  35235  cvmopnlem  35238  cvmliftlem14  35257  cvmliftlem15  35258  cvmlift2lem11  35273  cvmlift2lem12  35274  cvmlift2lem13  35275  cvmlift3lem2  35280  cvmlift3lem6  35284  cvmlift3lem9  35287  mthmi  35537  r1peuqusdeg1  35603  br8  35716  br6  35717  br4  35718  dfon2lem9  35752  wzel  35785  wsuclem  35786  wsuclb  35789  imagesset  35914  fvtransport  35993  brcolinear  36020  brsegle  36069  seglerflx  36073  seglemin  36074  btwnsegle  36078  fvray  36102  fvline  36105  hilbert1.1  36115  elhf2  36136  0hf  36138  nn0prpwlem  36283  nn0prpw  36284  fness  36310  fneref  36311  fnessref  36318  refssfne  36319  neibastop2lem  36321  fnemeet1  36327  tailfb  36338  filnetlem4  36342  limsucncmpi  36406  taupilemrplb  37281  relowlssretop  37324  rdgellim  37337  matunitlindflem2  37584  ptrecube  37587  poimirlem4  37591  poimirlem17  37604  poimirlem20  37607  poimirlem23  37610  poimirlem24  37611  poimirlem26  37613  poimirlem27  37614  poimirlem29  37616  poimirlem32  37619  heicant  37622  mblfinlem1  37624  mblfinlem2  37625  mblfinlem3  37626  mblfinlem4  37627  ismblfin  37628  volsupnfl  37632  itg2addnclem  37638  itg2addnclem3  37640  itg2addnc  37641  ftc1anclem5  37664  unirep  37681  cover2  37682  indexa  37700  frinfm  37702  sdclem1  37710  fdc  37712  incsequz  37715  caushft  37728  istotbnd3  37738  0totbnd  37740  sstotbnd2  37741  sstotbnd  37742  sstotbnd3  37743  isbnd3  37751  ssbnd  37755  equivbnd  37757  prdsbnd  37760  prdstotbnd  37761  cntotbnd  37763  heibor1lem  37776  heiborlem1  37778  heiborlem3  37780  heiborlem6  37783  heiborlem8  37785  bfplem2  37790  rrncmslem  37799  iccbnd  37807  opidonOLD  37819  exidres  37845  isrngod  37865  isgrpda  37922  isdrngo2  37925  igenval  38028  igenidl  38030  prtlem10  38831  lshpnel2N  38951  lsmsat  38974  lssatomic  38977  lcvnbtwn  38991  lfl1  39036  eqlkr  39065  lshpkrlem1  39076  lshpkrex  39084  cvrcon3b  39243  cvrat4  39410  3dim3  39436  ps-2  39445  llni  39475  llnle  39485  lplni  39499  lplnle  39507  lplnexllnN  39531  lvoli  39542  lnatexN  39746  elpaddn0  39767  pclfinN  39867  lhprelat3N  40007  4atexlemex2  40038  4atex  40043  4atex2-0aOLDN  40045  4atex2-0cOLDN  40047  lautcvr  40059  cdleme0ex1N  40190  cdleme50rnlem  40511  cdleme50ex  40526  cdlemg1cex  40555  cdlemkid5  40902  cdlemk  40941  tendoex  40942  cdleml5N  40947  cdlemm10N  41085  dih1dimatlem0  41295  dihjat1lem  41395  dvh3dim2  41415  dvh3dim3N  41416  dochkr1  41445  dochkr1OLDN  41446  lcfrvalsnN  41508  lcfrlem27  41536  lcfrlem37  41546  lcfr  41552  mapd1o  41615  mapdpglem23  41661  hdmap11lem2  41809  primrootsunit1  42058  zdivgd  42298  resubeu  42338  fidomncyc  42496  nacsfix  42673  mzpcompact2lem  42712  eldioph  42719  diophrw  42720  diophin  42733  rexrabdioph  42755  rexzrexnn0  42765  eldioph4b  42772  rencldnfilem  42781  irrapxlem5  42787  irrapxlem6  42788  pell1234qrdich  42822  pell14qrdich  42830  infmrgelbi  42839  pellqrex  42840  pellfundre  42842  pellfundlb  42845  rmxynorm  42880  congrep  42935  acongrep  42942  jm2.27  42970  fnwe2lem2  43013  islssfgi  43034  hbtlem2  43086  hbtlem4  43088  hbtlem5  43090  dgraaub  43110  mpaaeu  43112  aaitgo  43124  unielss  43180  onexgt  43202  onexomgt  43203  onexlimgt  43205  onexoegt  43206  oaordnr  43258  omnord1  43267  oenord1  43278  oaomoencom  43279  oenass  43281  tfsconcatfv2  43302  tfsconcatrn  43304  tfsconcatb0  43306  ofoafo  43318  naddcnffo  43326  oaun3lem1  43336  naddwordnexlem4  43363  sucomisnotcard  43506  clsk1independent  44008  0elaxnul  44946  pwclaxpow  44947  prclaxpr  44948  uniclaxun  44949  omssaxinf2  44951  wfac8prim  44965  restuni3  45085  iinssd  45098  founiiun  45146  wessf1ornlem  45152  founiiun0  45157  unirnmap  45175  dstregt0  45253  uzfissfz  45295  rpgtrecnn  45349  rexabslelem  45387  infrnmptle  45392  infxrunb3rnmpt  45397  infxrpnf  45415  supminfxr  45433  rexanuz2nf  45461  iooiinicc  45513  iooiinioc  45527  uzubioo  45536  climsuse  45579  islptre  45590  limsuppnfdlem  45672  climinf3  45687  limsupmnfuzlem  45697  limsupre3lem  45703  limsupre3uzlem  45706  0cnv  45713  liminfreuzlem  45773  cnrefiisplem  45800  icccncfext  45858  cncficcgt0  45859  dvbdfbdioo  45901  ioodvbdlimc1lem1  45902  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  stoweidlem9  45980  stoweidlem14  45985  stoweidlem18  45989  stoweidlem21  45992  stoweidlem29  46000  stoweidlem34  46005  stoweidlem35  46006  stoweidlem39  46010  stoweidlem41  46012  stoweidlem45  46016  stoweidlem52  46023  stoweidlem55  46026  stoweidlem57  46028  stoweidlem60  46031  stirlinglem5  46049  stirlinglem13  46057  stirlinglem14  46058  fourierdlem16  46094  fourierdlem20  46098  fourierdlem21  46099  fourierdlem22  46100  fourierdlem25  46103  fourierdlem31  46109  fourierdlem39  46117  fourierdlem41  46119  fourierdlem42  46120  fourierdlem47  46124  fourierdlem48  46125  fourierdlem49  46126  fourierdlem51  46128  fourierdlem63  46140  fourierdlem64  46141  fourierdlem65  46142  fourierdlem77  46154  fourierdlem81  46158  fourierdlem83  46160  fourierdlem103  46180  fourierdlem104  46181  elaa2lem  46204  etransclem47  46252  qndenserrnbl  46266  ioorrnopnlem  46275  ioorrnopnxrlem  46277  intsaluni  46300  salgencntex  46314  subsaliuncllem  46328  sge0resplit  46377  sge0seq  46417  sge0reuz  46418  nnfoctbdjlem  46426  meaiininclem  46457  hoicvrrex  46527  ovnlecvr  46529  ovnlerp  46533  hoidmv1lelem2  46563  hoidmvlelem2  46567  hoidmvlelem3  46568  ovnhoilem1  46572  ovnlecvr2  46581  hoiqssbl  46596  ovolval4lem2  46621  ovolval5lem2  46624  ovnovollem1  46627  ovnovollem2  46628  iinhoiicclem  46644  smfinflem  46788  smflimsuplem7  46797  sprsymrelfolem2  47467  perfectALTV  47697  9gbo  47748  11gbo  47749  nnsum3primes4  47762  nnsum3primesprm  47764  ssnn0ssfz  48310  lincsumcl  48393  lincscmcl  48394  zlmodzxzldep  48466  ldepsnlinc  48470  line2ylem  48713  line2xlem  48715  sepfsepc  48889  lubsscl  48921  glbsscl  48922  nelsubc3lem  49032  cnelsubclem  49565  aacllem  49763