Theorem rspcev 3560

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064

This theorem is referenced by:  rspcedvdw  3563  rspceaimv  3566  rspc2ev  3573  rspc3ev  3577  rspceeqv  3583  reu6i  3669  rspesbca  3813  eliuni  4928  iuneqconst  4934  brralrspcev  5133  wefrc  5613  wereu2  5616  xpdifid  6120  frpomin  6292  onfr  6350  onelssex  6360  ordunidif  6361  eliman0  6865  dffv2  6923  elrnrexdm  7031  eldmrexrn  7033  elabrex  7187  elabrexg  7188  f1elima  7208  fliftfun  7257  fliftval  7261  f1oiso2  7297  sorpssuni  7676  sorpssint  7677  onssmin  7736  onminex  7746  fimaproj  8076  frxp3  8092  poseq  8099  tfrlem12  8319  seqomlem2  8381  oawordeulem  8480  oaass  8487  odi  8505  omass  8506  omeulem1  8508  oen0  8513  oelim2  8522  oeeulem  8528  nnawordex  8564  nnaordex2  8566  eldifsucnn  8591  cofon1  8599  cofon2  8600  naddcllem  8603  naddunif  8620  boxcutc  8880  0fi  8980  snfi  8981  rexdif1en  9086  findcard  9089  nnfi  9093  pssnn  9094  unfi  9096  onfin  9140  dif1ennnALT  9178  frfi  9186  fisupg  9189  nnsdomg  9200  pwfir  9218  prfi  9225  fissuni  9258  fipreima  9259  finsschain  9260  indexfi  9261  marypha1lem  9337  eqsup  9360  supmax  9372  fisup2g  9373  fisupcl  9374  supisoex  9379  infmin  9400  fiinfg  9405  fiinf2g  9406  wofib  9451  wemaplem2  9453  card2inf  9461  brwdom2  9479  cnfcom3clem  9618  ssttrcl  9628  ttrcltr  9629  trcl  9641  frmin  9665  r1ordg  9694  r1pwss  9700  tz9.12lem3  9705  tz9.12  9706  r1elwf  9712  tcrank  9800  scottex  9801  scott0  9802  isnumi  9862  onsdom  9912  ondomen  9951  infpwfien  9976  cardaleph  10003  infenaleph  10005  alephfplem4  10021  alephfp2  10023  dfac2b  10045  ackbij1lem18  10150  ackbij1  10151  cflem  10159  cflemOLD  10160  cflecard  10167  cfsuc  10171  cfflb  10173  cofsmo  10183  coftr  10187  fin23lem7  10230  fin23lem11  10231  enfin2i  10235  fin23lem26  10239  isf32lem5  10271  isf34lem4  10291  isfin1-3  10300  fin1a2lem7  10320  axdc3lem4  10367  ttukeylem7  10429  iunfo  10453  ficard  10479  pwcfsdom  10498  fpwwe2lem11  10556  wunex  10654  eltsk2g  10666  grur1  10735  axgroth6  10743  inaprc  10751  nqereu  10844  archnq  10895  genpnmax  10922  ltexpri  10958  prlem936  10962  recexpr  10966  supexpr  10969  negexsr  11017  recexsrlem  11018  recexsr  11022  supsrlem  11026  axrnegex  11077  axrrecex  11078  axpre-sup  11084  1re  11136  dedekind  11301  dedekindle  11302  cnegex  11319  cnegex2  11320  recex  11774  receu  11787  fiminre2  12096  cju  12147  nn2ge  12196  nominpos  12406  zdiv  12591  btwnz  12624  uzwo  12853  ublbneg  12875  lbzbi  12878  zsupss  12879  uzsupss  12882  rpnnen1lem1  12920  rpnnen1lem3  12921  rpnnen1lem4  12922  rpnnen1lem5  12923  z2ge  13142  qbtwnre  13143  qbtwnxr  13144  xralrple  13149  xrsupsslem  13251  xrinfmsslem  13252  supxrpnf  13262  icc0  13338  uzsup  13814  expnbnd  14186  expmulnbnd  14189  hashkf  14286  hashdom  14333  iswrdi  14471  rtrclreclem1  15011  rtrclreclem2  15013  rtrclreclem3  15014  01sqrex  15203  resqrex  15204  sqrtneg  15221  abs1m  15290  rexanuz  15300  rexuz3  15303  rexuzre  15307  sqreu  15315  o1lo1  15491  climconst  15497  rlimclim1  15499  climshftlem  15528  rlimo1  15571  lo1add  15581  lo1mul  15582  lo1le  15606  isercoll  15622  serf0  15635  zsum  15672  fsum  15674  fsumcvg3  15683  mertenslem1  15841  ntrivcvgn0  15855  ntrivcvgmullem  15858  zprod  15894  fprod  15898  fprodntriv  15899  dvdsval2  16216  dvds0lem  16227  dvds1lem  16228  dvds2lem  16229  odd2np1lem  16301  odd2np1  16302  opeo  16326  omeo  16327  divalglem9  16362  gcdcllem3  16462  lcmcllem  16557  qredeu  16619  exprmfct  16666  isprm5  16669  odzcllem  16755  reumodprminv  16767  modprm0  16768  nnnn0modprm0  16769  pythagtriplem19  16796  pcprmpw2  16845  pockthi  16870  infpnlem2  16874  vdwlem2  16945  vdwlem10  16953  vdwlem13  16956  ramub1lem1  16989  cshwrepswhash1  17065  imasleval  17497  mreexexlem3d  17604  mreexexlem4d  17605  iscatd  17631  cat1  18056  poslubd  18369  fpwipodrs  18498  ismgmid2  18628  mgmidsssn0  18632  gsumval2a  18645  ismndd  18716  isgrpd2  18924  isgrpd  18926  imasgrp2  19023  mhmmnd  19032  ghmgrp  19034  gaorber  19275  orbsta  19280  cayleyth  19382  pmtrdifel  19447  pmtrdifwrdel  19452  pmtrdifwrdel2  19453  psgnunilem2  19462  psgnunilem3  19463  psgnvalii  19476  pgpfi1  19562  sylow1lem3  19567  sylow1lem5  19569  pgpfi  19572  sylow2alem2  19585  efgredeu  19719  lt6abl  19862  pgpfac1lem3a  20045  pgpfac1lem3  20046  pgpfac1lem5  20048  pgpfaclem1  20050  pgpfaclem3  20052  ablfaclem2  20055  dvdsrmul  20336  dvdsr01  20343  irredrmul  20399  rhmdvdsr  20481  rgspnval  20585  rgspncl  20586  lspf  20965  lspval  20966  lssats2  20991  lspfixed  21122  lspsolvlem  21136  zringlpir  21443  pzriprnglem13  21469  zncyg  21524  cygth  21547  frlmup4  21777  aspval  21848  evlseu  22060  fiinbas  22936  topbas  22956  pptbas  22992  clsval  23021  elcls  23057  neiint  23088  neips  23097  opnneissb  23098  opnssneib  23099  innei  23109  neiptopnei  23116  restbas  23142  neitr  23164  pnfnei  23204  mnfnei  23205  lmconst  23245  iscnp4  23247  cncnpi  23262  cnconst2  23267  cnprest  23273  cnpdis  23277  nrmsep  23341  regsep2  23360  cmpcovf  23375  cmpsub  23384  cmpcld  23386  hauscmplem  23390  conncompid  23415  2ndci  23432  2ndcsb  23433  2ndc1stc  23435  1stcrest  23437  2ndcctbss  23439  2ndcdisj  23440  2ndcomap  23442  2ndcsep  23443  dis2ndc  23444  restlly  23467  islly2  23468  hausllycmp  23478  cldllycmp  23479  lly1stc  23480  dislly  23481  ssref  23496  refref  23497  finlocfin  23504  dissnlocfin  23513  locfindis  23514  llycmpkgen2  23534  cmpkgen  23535  1stckgenlem  23537  elptr  23557  ptbasfi  23565  neitx  23591  ptpjopn  23596  txcnp  23604  ptcnplem  23605  txlly  23620  txnlly  23621  txtube  23624  txcmplem1  23625  tx1stc  23634  txkgen  23636  xkococnlem  23643  txconn  23673  tgqtop  23696  kqreglem1  23725  kqreglem2  23726  kqnrmlem1  23727  kqnrmlem2  23728  reghmph  23777  nrmhmph  23778  fbssfi  23821  opnfbas  23826  isfil2  23840  fsubbas  23851  ssfg  23856  fgss2  23858  fbasrn  23868  filuni  23869  fgtr  23874  ssufl  23902  uffix  23905  elfm2  23932  elfm3  23934  imaelfm  23935  rnelfmlem  23936  rnelfm  23937  fmfnfmlem4  23941  fmfnfm  23942  fmco  23945  ufldom  23946  hausflim  23965  flimcls  23969  hauspwpwf1  23971  flffbas  23979  txflf  23990  fclscf  24009  fclsfnflim  24011  alexsubALTlem4  24034  alexsubALT  24035  tmdgsum2  24080  symgtgp  24090  subgntr  24091  opnsubg  24092  ghmcnp  24099  qustgpopn  24104  tsmsfbas  24112  tsmsxplem1  24137  ustexsym  24200  trust  24213  utoptop  24218  restutop  24221  restutopopn  24222  ustuqtop4  24228  utopsnneiplem  24231  iducn  24266  fmucnd  24275  cfilufg  24276  trcfilu  24277  neipcfilu  24279  imasdsf1olem  24357  blssps  24408  blss  24409  blssexps  24410  blssex  24411  ssblex  24412  blin2  24413  neibl  24485  blcld  24489  metss2  24496  stdbdmopn  24502  met1stc  24505  met2ndci  24506  metrest  24508  prdsxmslem2  24513  metcnp3  24524  metustexhalf  24540  metustfbas  24541  cfilucfil  24543  restmetu  24554  dscopn  24557  ngptgp  24620  nlmvscnlem1  24670  tgioo  24780  tgqioo  24784  xrsmopn  24797  zcld  24798  recld2  24799  zdis  24801  icccmplem1  24807  icccmplem2  24808  xmetdcn2  24822  addcnlem  24849  xrhmeo  24932  cnheibor  24941  cnllycmp  24942  lebnumlem3  24949  lebnum  24950  xlebnum  24951  lebnumii  24952  elpi1i  25032  ipcnlem1  25231  lmnn  25249  iscfil3  25259  cfilres  25282  flimcfil  25300  bcthlem4  25313  bcthlem5  25314  minveclem4c  25411  minveclem2  25412  minveclem3b  25414  minveclem3  25415  minveclem4  25418  minveclem6  25420  ivthlem2  25438  ivth  25440  ivthle  25442  ivthle2  25443  elovolmr  25462  ovolunlem1  25483  ovoliunlem2  25489  ovolicc1  25502  iundisj  25534  iunmbl2  25543  dyadmbllem  25585  volivth  25593  mbflimsup  25652  i1faddlem  25679  i1fmullem  25680  itg2lr  25716  itg2monolem1  25736  limcnlp  25864  ellimc3  25865  limcflf  25867  limciun  25880  rollelem  25975  c1lip1  25983  lhop1lem  25999  ply1divex  26121  ig1peu  26159  elply2  26180  coeeq  26211  plydivlem3  26280  plydivlem4  26281  elqaalem3  26306  qaa  26308  iaa  26310  aareccl  26311  aannenlem2  26314  aalioulem2  26318  aalioulem3  26319  aalioulem5  26321  aalioulem6  26322  aaliou  26323  aaliou2  26325  aaliou3lem8  26330  ulmshftlem  26373  reeff1o  26431  pilem2  26436  pilem3  26437  efif1olem2  26526  efopn  26641  cxpcn3lem  26730  cxpeq  26740  dcubic2  26827  quart  26844  xrlimcnp  26951  ftalem5  27059  ftalem7  27061  sgmnncl  27129  dvdsppwf1o  27168  musum  27173  perfect  27213  dchrptlem1  27246  dchrptlem2  27247  dchrpt  27249  bpos1lem  27264  lgsqrlem4  27331  lgsdchrval  27336  2sqblem  27413  dchrisumlem3  27473  chpdifbndlem2  27536  pntrsumbnd2  27549  pntpbnd1  27568  pntpbnd2  27569  pntpbnd  27570  pntibndlem2  27573  pntibndlem3  27574  pntleme  27590  pntlem3  27591  elno2  27637  ltsval2  27639  noreson  27643  ltsres  27645  noseponlem  27647  nolesgn2o  27654  nogesgn1o  27656  nodense  27675  nosupfv  27689  nosupres  27690  nosupbnd1lem3  27693  nosupbnd1lem5  27695  nosupbnd2lem1  27698  noinffv  27704  noinfres  27705  noinfbnd1lem3  27708  noinfbnd1lem5  27710  noinfbnd2lem1  27713  noetasuplem4  27719  noetainflem4  27723  noetalem2  27725  cuteq0  27826  cuteq1  27828  oldlim  27898  bdayiun  27926  cofcutrtime  27938  cofss  27941  coiniss  27942  cutlt  27943  cutmax  27945  cutmin  27946  negsex  28054  negsfo  28064  norecdiv  28201  divs1  28215  precsexlem11  28228  precsex  28229  recsex  28230  elons2d  28270  oncutlt  28275  n0on  28347  bdayn0sf1o  28381  dfnns2  28383  zsoring  28420  pw2recs  28449  halfcut  28469  0reno  28507  1reno  28508  readdscl  28510  axtgcont  28556  tgcgrxfr  28605  legid  28674  btwnleg  28675  leg0  28679  tghilberti1  28724  tglnpt2  28728  colline  28736  mirreu3  28741  isperp2  28802  colperpex  28820  lnopp2hpgb  28850  hpgerlem  28852  brbtwn  28987  brcgr  28988  brbtwn2  28993  axpasch  29029  axlowdimlem14  29043  axlowdim2  29048  axcontlem2  29053  axcontlem4  29055  axcontlem8  29059  axcontlem10  29061  axcontlem12  29063  fusgrn0degnn0  29587  friendshipgt3  30487  lpni  30570  isgrpoi  30588  vacn  30784  smcnlem  30787  nmosetn0  30855  nmoolb  30861  nmobndi  30865  nmoo0  30881  nmlno0lem  30883  isblo3i  30891  blo3i  30892  blocnilem  30894  ubthlem1  30960  minvecolem2  30965  minvecolem3  30966  minvecolem4c  30969  minvecolem4  30970  minvecolem5  30971  minvecolem6  30972  norm1exi  31340  occl  31394  spanval  31423  spancl  31426  shsval2i  31477  ococin  31498  pjoml6i  31679  nmopsetn0  31955  nmfnsetn0  31968  nmoplb  31997  nmfnlb  32014  nmop0  32076  nmfn0  32077  nmlnop0iALT  32085  nmopun  32104  nmcexi  32116  lnconi  32123  lnopcnbd  32126  lnfncnbd  32147  riesz3i  32152  riesz1  32155  cnlnadjlem2  32158  cnlnadjlem8  32164  cnlnadjlem9  32165  adjbd1o  32175  branmfn  32195  opsqrlem1  32230  pjnmopi  32238  strlem1  32340  stri  32347  hstri  32355  cvcon3  32374  cvnbtwn  32376  superpos  32444  shatomici  32448  atcvat4i  32487  mdsymlem2  32494  cdj1i  32523  cdj3i  32531  rexunirn  32580  foresf1o  32593  iundisjf  32679  aciunf1lem  32755  fnpreimac  32763  fgreu  32764  fcnvgreu  32765  xrge0infss  32853  ssnnssfz  32880  iundisjfi  32889  indf1ofs  32946  xreceu  33001  rexdiv  33005  isarchi3  33269  archirngz  33271  archiabllem2a  33276  0nellinds  33454  qtophaus  34029  reff  34032  locfinreflem  34033  cmpcref  34043  dispcmp  34052  tpr2rico  34105  pnfneige0  34144  qqhucn  34185  rrhre  34214  esumcst  34256  esumpcvgval  34271  dmsigagen  34337  rossros  34373  dya2icoseg  34470  dya2iocnrect  34474  dya2iocuni  34476  eulerpartlemgvv  34569  dstfrvunirn  34668  ballotlem4  34692  ballotlemic  34700  ballotlem1c  34701  ballotlemrc  34724  signsw0g  34749  signswmnd  34750  prodfzo03  34796  tgoldbachgt  34856  onvf1odlem4  35343  loop1cycl  35374  umgr2cycllem  35377  umgr2cycl  35378  subfacp1lem3  35419  erdsze2lem2  35441  cnpconn  35467  txpconn  35469  ptpconn  35470  indispconn  35471  connpconn  35472  cvxpconn  35479  cnllysconn  35482  cvmsss2  35511  cvmcov2  35512  cvmopnlem  35515  cvmliftlem14  35534  cvmliftlem15  35535  cvmlift2lem11  35550  cvmlift2lem12  35551  cvmlift2lem13  35552  cvmlift3lem2  35557  cvmlift3lem6  35561  cvmlift3lem9  35564  mthmi  35814  r1peuqusdeg1  35880  br8  35993  br6  35994  br4  35995  dfon2lem9  36026  wzel  36059  wsuclem  36060  wsuclb  36063  imagesset  36190  fvtransport  36269  brcolinear  36296  brsegle  36345  seglerflx  36349  seglemin  36350  btwnsegle  36354  fvray  36378  fvline  36381  hilbert1.1  36391  elhf2  36412  0hf  36414  nn0prpwlem  36559  nn0prpw  36560  fness  36586  fneref  36587  fnessref  36594  refssfne  36595  neibastop2lem  36597  fnemeet1  36603  tailfb  36614  filnetlem4  36618  limsucncmpi  36682  ttctr  36730  dfttc2g  36743  taupilemrplb  37689  qdiff  37696  relowlssretop  37734  rdgellim  37747  matunitlindflem2  37993  ptrecube  37996  poimirlem4  38000  poimirlem17  38013  poimirlem20  38016  poimirlem23  38019  poimirlem24  38020  poimirlem26  38022  poimirlem27  38023  poimirlem29  38025  poimirlem32  38028  heicant  38031  mblfinlem1  38033  mblfinlem2  38034  mblfinlem3  38035  mblfinlem4  38036  ismblfin  38037  volsupnfl  38041  itg2addnclem  38047  itg2addnclem3  38049  itg2addnc  38050  ftc1anclem5  38073  unirep  38090  cover2  38091  indexa  38109  frinfm  38111  sdclem1  38119  fdc  38121  incsequz  38124  caushft  38137  istotbnd3  38147  0totbnd  38149  sstotbnd2  38150  sstotbnd  38151  sstotbnd3  38152  isbnd3  38160  ssbnd  38164  equivbnd  38166  prdsbnd  38169  prdstotbnd  38170  cntotbnd  38172  heibor1lem  38185  heiborlem1  38187  heiborlem3  38189  heiborlem6  38192  heiborlem8  38194  bfplem2  38199  rrncmslem  38208  iccbnd  38216  opidonOLD  38228  exidres  38254  isrngod  38274  isgrpda  38331  isdrngo2  38334  igenval  38437  igenidl  38439  prtlem10  39366  lshpnel2N  39486  lsmsat  39509  lssatomic  39512  lcvnbtwn  39526  lfl1  39571  eqlkr  39600  lshpkrlem1  39611  lshpkrex  39619  cvrcon3b  39778  cvrat4  39944  3dim3  39970  ps-2  39979  llni  40009  llnle  40019  lplni  40033  lplnle  40041  lplnexllnN  40065  lvoli  40076  lnatexN  40280  elpaddn0  40301  pclfinN  40401  lhprelat3N  40541  4atexlemex2  40572  4atex  40577  4atex2-0aOLDN  40579  4atex2-0cOLDN  40581  lautcvr  40593  cdleme0ex1N  40724  cdleme50rnlem  41045  cdleme50ex  41060  cdlemg1cex  41089  cdlemkid5  41436  cdlemk  41475  tendoex  41476  cdleml5N  41481  cdlemm10N  41619  dih1dimatlem0  41829  dihjat1lem  41929  dvh3dim2  41949  dvh3dim3N  41950  dochkr1  41979  dochkr1OLDN  41980  lcfrvalsnN  42042  lcfrlem27  42070  lcfrlem37  42080  lcfr  42086  mapd1o  42149  mapdpglem23  42195  hdmap11lem2  42343  primrootsunit1  42591  zdivgd  42823  resubeu  42863  fidomncyc  43030  nacsfix  43170  mzpcompact2lem  43209  eldioph  43216  diophrw  43217  diophin  43230  rexrabdioph  43248  rexzrexnn0  43258  eldioph4b  43265  rencldnfilem  43274  irrapxlem5  43280  irrapxlem6  43281  pell1234qrdich  43315  pell14qrdich  43323  infmrgelbi  43332  pellqrex  43333  pellfundre  43335  pellfundlb  43338  rmxynorm  43372  congrep  43427  acongrep  43434  jm2.27  43462  fnwe2lem2  43505  islssfgi  43526  hbtlem2  43578  hbtlem4  43580  hbtlem5  43582  dgraaub  43602  mpaaeu  43604  aaitgo  43616  unielss  43672  onexgt  43694  onexomgt  43695  onexlimgt  43697  onexoegt  43698  oaordnr  43750  omnord1  43759  oenord1  43770  oaomoencom  43771  oenass  43773  tfsconcatfv2  43794  tfsconcatrn  43796  tfsconcatb0  43798  ofoafo  43810  naddcnffo  43818  oaun3lem1  43828  naddwordnexlem4  43855  sucomisnotcard  43997  clsk1independent  44499  0elaxnul  45436  pwclaxpow  45437  prclaxpr  45438  uniclaxun  45439  omssaxinf2  45441  wfac8prim  45455  restuni3  45573  iinssd  45586  founiiun  45634  wessf1ornlem  45640  founiiun0  45645  unirnmap  45661  dstregt0  45738  uzfissfz  45779  rpgtrecnn  45832  rexabslelem  45869  infrnmptle  45874  infxrunb3rnmpt  45879  infxrpnf  45897  supminfxr  45915  rexanuz2nf  45943  iooiinicc  45995  iooiinioc  46009  uzubioo  46018  climsuse  46061  islptre  46072  limsuppnfdlem  46152  climinf3  46167  limsupmnfuzlem  46177  limsupre3lem  46183  limsupre3uzlem  46186  0cnv  46193  liminfreuzlem  46253  cnrefiisplem  46280  icccncfext  46338  cncficcgt0  46339  dvbdfbdioo  46381  ioodvbdlimc1lem1  46382  ioodvbdlimc1lem2  46383  ioodvbdlimc2lem  46385  stoweidlem9  46460  stoweidlem14  46465  stoweidlem18  46469  stoweidlem21  46472  stoweidlem29  46480  stoweidlem34  46485  stoweidlem35  46486  stoweidlem39  46490  stoweidlem41  46492  stoweidlem45  46496  stoweidlem52  46503  stoweidlem55  46506  stoweidlem57  46508  stoweidlem60  46511  stirlinglem5  46529  stirlinglem13  46537  stirlinglem14  46538  fourierdlem16  46574  fourierdlem20  46578  fourierdlem21  46579  fourierdlem22  46580  fourierdlem25  46583  fourierdlem31  46589  fourierdlem39  46597  fourierdlem41  46599  fourierdlem42  46600  fourierdlem47  46604  fourierdlem48  46605  fourierdlem49  46606  fourierdlem51  46608  fourierdlem63  46620  fourierdlem64  46621  fourierdlem65  46622  fourierdlem77  46634  fourierdlem81  46638  fourierdlem83  46640  fourierdlem103  46660  fourierdlem104  46661  elaa2lem  46684  etransclem47  46732  qndenserrnbl  46746  ioorrnopnlem  46755  ioorrnopnxrlem  46757  intsaluni  46780  salgencntex  46794  subsaliuncllem  46808  sge0resplit  46857  sge0seq  46897  sge0reuz  46898  nnfoctbdjlem  46906  meaiininclem  46937  hoicvrrex  47007  ovnlecvr  47009  ovnlerp  47013  hoidmv1lelem2  47043  hoidmvlelem2  47047  hoidmvlelem3  47048  ovnhoilem1  47052  ovnlecvr2  47061  hoiqssbl  47076  ovolval4lem2  47101  ovolval5lem2  47104  ovnovollem1  47107  ovnovollem2  47108  iinhoiicclem  47124  smfinflem  47268  smflimsuplem7  47277  nthrucw  47339  sprsymrelfolem2  47976  perfectALTV  48222  9gbo  48273  11gbo  48274  nnsum3primes4  48287  nnsum3primesprm  48289  ssnn0ssfz  48848  lincsumcl  48930  lincscmcl  48931  zlmodzxzldep  49003  ldepsnlinc  49007  line2ylem  49250  line2xlem  49252  sepfsepc  49426  lubsscl  49458  glbsscl  49459  nelsubc3lem  49568  cnelsubclem  50101  aacllem  50299