Theorem rspcev 3582

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1561   ∈ wcel 2143  ∃wrex 3087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1564  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3078  df-rex 3088

This theorem is referenced by:  rspcedvdw  3585  rspceaimv  3588  rspc2ev  3595  rspc3ev  3599  rspceeqv  3605  reu6i  3692  rspesbca  3835  eliuni  4956  iuneqconst  4962  brralrspcev  5161  wefrc  5642  wereu2  5645  xpdifid  6154  xpdifcnvepel  6155  frpomin  6328  onfr  6386  onelssex  6396  ordunidif  6397  eliman0  6905  dffv2  6963  elrnrexdm  7071  eldmrexrn  7073  elabrex  7227  elabrexg  7228  f1elima  7248  fliftfun  7297  fliftval  7301  f1oiso2  7337  sorpssuni  7716  sorpssint  7717  onssmin  7776  onminex  7786  fimaproj  8116  frxp3  8132  poseq  8139  tfrlem12  8361  seqomlem2  8423  oawordeulem  8524  oaass  8531  odi  8549  omass  8550  omeulem1  8552  oen0  8557  oelim2  8566  oeeulem  8572  nnawordex  8608  nnaordex2  8610  eldifsucnn  8635  cofon1  8643  cofon2  8644  naddcllem  8647  naddunif  8665  boxcutc  8924  0fi  9024  snfi  9025  rexdif1en  9130  findcard  9133  nnfi  9137  pssnn  9138  unfi  9140  onfin  9184  dif1ennnALT  9222  frfi  9230  fisupg  9233  nnsdomg  9244  pwfir  9262  prfi  9269  fissuni  9301  fipreima  9302  finsschain  9303  indexfi  9304  marypha1lem  9380  eqsup  9403  supmax  9415  fisup2g  9416  fisupcl  9417  supisoex  9422  infmin  9443  fiinfg  9448  fiinf2g  9449  wofib  9494  wemaplem2  9496  card2inf  9504  brwdom2  9522  cnfcom3clem  9661  ssttrcl  9671  ttrcltr  9672  trcl  9684  frmin  9708  r1ordg  9737  r1pwss  9743  tz9.12lem3  9748  tz9.12  9749  r1elwf  9755  tcrank  9843  scottex  9844  scott0  9845  isnumi  9905  onsdom  9955  ondomen  9994  infpwfien  10019  cardaleph  10046  infenaleph  10048  alephfplem4  10064  alephfp2  10066  dfac2b  10088  ackbij1lem18  10193  ackbij1  10194  cflem  10202  cflemOLD  10203  cflecard  10210  cfsuc  10215  cfflb  10217  cofsmo  10227  coftr  10231  fin23lem7  10274  fin23lem11  10275  enfin2i  10279  fin23lem26  10283  isf32lem5  10315  isf34lem4  10335  isfin1-3  10344  fin1a2lem7  10364  axdc3lem4  10411  ttukeylem7  10473  iunfo  10497  ficard  10523  pwcfsdom  10542  fpwwe2lem11  10600  wunex  10698  eltsk2g  10710  grur1  10779  axgroth6  10787  inaprc  10795  nqereu  10888  archnq  10939  genpnmax  10966  ltexpri  11002  prlem936  11006  recexpr  11010  supexpr  11013  negexsr  11061  recexsrlem  11062  recexsr  11066  supsrlem  11070  axrnegex  11121  axrrecex  11122  axpre-sup  11128  1re  11182  dedekind  11347  dedekindle  11348  cnegex  11365  cnegex2  11366  recex  11820  receu  11833  fiminre2  12141  cju  12192  nn2ge  12241  nominpos  12459  zdiv  12644  btwnz  12677  uzwo  12913  ublbneg  12935  lbzbi  12938  zsupss  12939  uzsupss  12942  rpnnen1lem1  12980  rpnnen1lem3  12981  rpnnen1lem4  12982  rpnnen1lem5  12983  z2ge  13202  qbtwnre  13203  qbtwnxr  13204  xralrple  13209  xrsupsslem  13311  xrinfmsslem  13312  supxrpnf  13322  icc0  13398  uzsup  13874  expnbnd  14246  expmulnbnd  14249  hashkf  14346  hashdom  14393  iswrdi  14531  rtrclreclem1  15071  rtrclreclem2  15073  rtrclreclem3  15074  01sqrex  15277  resqrex  15278  sqrtneg  15295  abs1m  15364  rexanuz  15374  rexuz3  15377  rexuzre  15381  sqreu  15389  o1lo1  15565  climconst  15571  rlimclim1  15573  climshftlem  15602  rlimo1  15645  lo1add  15655  lo1mul  15656  lo1le  15680  isercoll  15696  serf0  15709  zsum  15746  fsum  15748  fsumcvg3  15757  mertenslem1  15915  ntrivcvgn0  15929  ntrivcvgmullem  15932  zprod  15968  fprod  15972  fprodntriv  15973  dvdsval2  16290  dvds0lem  16301  dvds1lem  16302  dvds2lem  16303  odd2np1lem  16375  odd2np1  16376  opeo  16400  omeo  16401  divalglem9  16436  gcdcllem3  16536  lcmcllem  16631  qredeu  16693  exprmfct  16740  isprm5  16743  odzcllem  16829  reumodprminv  16841  modprm0  16842  nnnn0modprm0  16843  pythagtriplem19  16870  pcprmpw2  16919  pockthi  16944  infpnlem2  16948  vdwlem2  17019  vdwlem10  17027  vdwlem13  17030  ramub1lem1  17063  cshwrepswhash1  17139  imasleval  17572  mreexexlem3d  17679  mreexexlem4d  17680  iscatd  17706  cat1  18131  poslubd  18444  fpwipodrs  18573  ismgmid2  18703  mgmidsssn0  18707  gsumval2a  18720  ismndd  18791  isgrpd2  18999  isgrpd  19001  imasgrp2  19098  mhmmnd  19107  ghmgrp  19109  gaorber  19349  orbsta  19354  cayleyth  19456  pmtrdifel  19521  pmtrdifwrdel  19526  pmtrdifwrdel2  19527  psgnunilem2  19536  psgnunilem3  19537  psgnvalii  19550  pgpfi1  19636  sylow1lem3  19641  sylow1lem5  19643  pgpfi  19646  sylow2alem2  19659  efgredeu  19793  lt6abl  19936  pgpfac1lem3a  20119  pgpfac1lem3  20120  pgpfac1lem5  20122  pgpfaclem1  20124  pgpfaclem3  20126  ablfaclem2  20129  dvdsrmul  20414  dvdsr01  20421  irredrmul  20477  rhmdvdsr  20559  rgspnval  20663  rgspncl  20664  lspf  21042  lspval  21043  lssats2  21068  lspfixed  21199  lspsolvlem  21213  zringlpir  21520  pzriprnglem13  21546  zncyg  21601  cygth  21624  frlmup4  21854  aspval  21925  evlseu  22137  fiinbas  23013  topbas  23033  pptbas  23069  clsval  23098  elcls  23134  neiint  23165  neips  23174  opnneissb  23175  opnssneib  23176  innei  23186  neiptopnei  23193  restbas  23219  neitr  23241  pnfnei  23281  mnfnei  23282  lmconst  23322  iscnp4  23324  cncnpi  23339  cnconst2  23344  cnprest  23350  cnpdis  23354  nrmsep  23418  regsep2  23437  cmpcovf  23452  cmpsub  23461  cmpcld  23463  hauscmplem  23467  conncompid  23492  2ndci  23509  2ndcsb  23510  2ndc1stc  23512  1stcrest  23514  2ndcctbss  23516  2ndcdisj  23517  2ndcomap  23519  2ndcsep  23520  dis2ndc  23521  restlly  23544  islly2  23545  hausllycmp  23555  cldllycmp  23556  lly1stc  23557  dislly  23558  ssref  23573  refref  23574  finlocfin  23581  dissnlocfin  23590  locfindis  23591  llycmpkgen2  23611  cmpkgen  23612  1stckgenlem  23614  elptr  23634  ptbasfi  23642  neitx  23668  ptpjopn  23673  txcnp  23681  ptcnplem  23682  txlly  23697  txnlly  23698  txtube  23701  txcmplem1  23702  tx1stc  23711  txkgen  23713  xkococnlem  23720  txconn  23750  tgqtop  23773  kqreglem1  23802  kqreglem2  23803  kqnrmlem1  23804  kqnrmlem2  23805  reghmph  23854  nrmhmph  23855  fbssfi  23898  opnfbas  23903  isfil2  23917  fsubbas  23928  ssfg  23933  fgss2  23935  fbasrn  23945  filuni  23946  fgtr  23951  ssufl  23979  uffix  23982  elfm2  24009  elfm3  24011  imaelfm  24012  rnelfmlem  24013  rnelfm  24014  fmfnfmlem4  24018  fmfnfm  24019  fmco  24022  ufldom  24023  hausflim  24042  flimcls  24046  hauspwpwf1  24048  flffbas  24056  txflf  24067  fclscf  24086  fclsfnflim  24088  alexsubALTlem4  24111  alexsubALT  24112  tmdgsum2  24157  symgtgp  24167  subgntr  24168  opnsubg  24169  ghmcnp  24176  qustgpopn  24181  tsmsfbas  24189  tsmsxplem1  24214  ustexsym  24277  trust  24290  utoptop  24295  restutop  24298  restutopopn  24299  ustuqtop4  24305  utopsnneiplem  24308  iducn  24343  fmucnd  24352  cfilufg  24353  trcfilu  24354  neipcfilu  24356  imasdsf1olem  24434  blssps  24485  blss  24486  blssexps  24487  blssex  24488  ssblex  24489  blin2  24490  neibl  24562  blcld  24566  metss2  24573  stdbdmopn  24579  met1stc  24582  met2ndci  24583  metrest  24585  prdsxmslem2  24590  metcnp3  24601  metustexhalf  24617  metustfbas  24618  cfilucfil  24620  restmetu  24631  dscopn  24634  ngptgp  24697  nlmvscnlem1  24747  tgioo  24857  tgqioo  24861  xrsmopn  24874  zcld  24875  recld2  24876  zdis  24878  icccmplem1  24884  icccmplem2  24885  xmetdcn2  24899  addcnlem  24926  xrhmeo  25009  cnheibor  25018  cnllycmp  25019  lebnumlem3  25026  lebnum  25027  xlebnum  25028  lebnumii  25029  elpi1i  25109  ipcnlem1  25308  lmnn  25326  iscfil3  25336  cfilres  25359  flimcfil  25377  bcthlem4  25390  bcthlem5  25391  minveclem4c  25488  minveclem2  25489  minveclem3b  25491  minveclem3  25492  minveclem4  25495  minveclem6  25497  ivthlem2  25515  ivth  25517  ivthle  25519  ivthle2  25520  elovolmr  25539  ovolunlem1  25560  ovoliunlem2  25566  ovolicc1  25579  iundisj  25611  iunmbl2  25620  dyadmbllem  25662  volivth  25670  mbflimsup  25729  i1faddlem  25756  i1fmullem  25757  itg2lr  25793  itg2monolem1  25813  limcnlp  25941  ellimc3  25942  limcflf  25944  limciun  25957  rollelem  26052  c1lip1  26060  lhop1lem  26076  ply1divex  26198  ig1peu  26236  elply2  26257  coeeq  26288  plydivlem3  26360  plydivlem4  26361  elqaalem3  26386  qaa  26388  iaa  26390  aareccl  26391  aannenlem2  26394  aalioulem2  26398  aalioulem3  26399  aalioulem5  26401  aalioulem6  26402  aaliou  26403  aaliou2  26405  aaliou3lem8  26410  ulmshftlem  26453  reeff1o  26511  pilem2  26516  pilem3  26517  efif1olem2  26609  efopn  26724  cxpcn3lem  26813  cxpeq  26823  dcubic2  26910  quart  26927  xrlimcnp  27034  ftalem5  27142  ftalem7  27144  sgmnncl  27212  dvdsppwf1o  27251  musum  27256  perfect  27296  dchrptlem1  27329  dchrptlem2  27330  dchrpt  27332  bpos1lem  27347  lgsqrlem4  27414  lgsdchrval  27419  2sqblem  27496  dchrisumlem3  27556  chpdifbndlem2  27619  pntrsumbnd2  27632  pntpbnd1  27651  pntpbnd2  27652  pntpbnd  27653  pntibndlem2  27656  pntibndlem3  27657  pntleme  27673  pntlem3  27674  elno2  27719  ltsval2  27721  noreson  27725  ltsres  27727  noseponlem  27729  nolesgn2o  27736  nogesgn1o  27738  nodense  27757  nosupfv  27771  nosupres  27772  nosupbnd1lem3  27775  nosupbnd1lem5  27777  nosupbnd2lem1  27780  noinffv  27786  noinfres  27787  noinfbnd1lem3  27790  noinfbnd1lem5  27792  noinfbnd2lem1  27795  noetasuplem4  27801  noetainflem4  27805  noetalem2  27807  cuteq0  27909  cuteq1  27911  oldlim  27981  bdayiun  28009  cofcutrtime  28021  cofss  28024  coiniss  28025  cutlt  28026  cutmax  28028  cutmin  28029  negsex  28137  negsfo  28147  norecdiv  28284  divs1  28298  precsexlem11  28311  precsex  28312  recsex  28313  elons2d  28353  oncutlt  28358  n0on  28430  bdayn0sf1o  28464  dfnns2  28466  zsoring  28503  pw2recs  28532  halfcut  28552  0reno  28590  1reno  28591  readdscl  28593  axtgcont  28639  tgcgrxfr  28688  legid  28757  btwnleg  28758  leg0  28762  tghilberti1  28807  colline  28820  mirreu3  28828  isperp2  28889  colperpex  28907  lnopp2hpgb  28937  hpgerlem  28939  brbtwn  29101  brcgr  29102  brbtwn2  29107  axpasch  29143  axlowdimlem14  29157  axlowdim2  29162  axcontlem2  29167  axcontlem4  29169  axcontlem8  29173  axcontlem10  29175  axcontlem12  29177  fusgrn0degnn0  29701  friendshipgt3  30601  lpni  30684  isgrpoi  30702  vacn  30898  smcnlem  30901  nmosetn0  30969  nmoolb  30975  nmobndi  30979  nmoo0  30995  nmlno0lem  30997  isblo3i  31005  blo3i  31006  blocnilem  31008  ubthlem1  31074  minvecolem2  31079  minvecolem3  31080  minvecolem4c  31083  minvecolem4  31084  minvecolem5  31085  minvecolem6  31086  norm1exi  31454  occl  31508  spanval  31537  spancl  31540  shsval2i  31591  ococin  31612  pjoml6i  31793  nmopsetn0  32069  nmfnsetn0  32082  nmoplb  32111  nmfnlb  32128  nmop0  32190  nmfn0  32191  nmlnop0iALT  32199  nmopun  32218  nmcexi  32230  lnconi  32237  lnopcnbd  32240  lnfncnbd  32261  riesz3i  32266  riesz1  32269  cnlnadjlem2  32272  cnlnadjlem8  32278  cnlnadjlem9  32279  adjbd1o  32289  branmfn  32309  opsqrlem1  32344  pjnmopi  32352  strlem1  32454  stri  32461  hstri  32469  cvcon3  32488  cvnbtwn  32490  superpos  32558  shatomici  32562  atcvat4i  32601  mdsymlem2  32608  cdj1i  32637  cdj3i  32645  rexunirn  32692  foresf1o  32704  iundisjf  32790  aciunf1lem  32865  fnpreimac  32873  fgreu  32874  fcnvgreu  32875  xrge0infss  32963  ssnnssfz  32990  iundisjfi  32999  indf1ofs  33045  xreceu  33100  rexdiv  33104  isarchi3  33368  archirngz  33370  archiabllem2a  33375  0nellinds  33557  qtophaus  34134  reff  34137  locfinreflem  34138  cmpcref  34148  dispcmp  34157  tpr2rico  34210  pnfneige0  34249  qqhucn  34290  rrhre  34319  esumcst  34361  esumpcvgval  34376  dmsigagen  34442  rossros  34478  dya2icoseg  34575  dya2iocnrect  34579  dya2iocuni  34581  eulerpartlemgvv  34674  dstfrvunirn  34773  ballotlem4  34797  ballotlemic  34805  ballotlemrc  34829  signsw0g  34851  signswmnd  34852  prodfzo03  34898  tgoldbachgt  34958  onvf1odlem4  35450  loop1cycl  35488  umgr2cycllem  35491  umgr2cycl  35492  subfacp1lem3  35533  erdsze2lem2  35555  cnpconn  35581  txpconn  35583  ptpconn  35584  indispconn  35585  connpconn  35586  cvxpconn  35593  cnllysconn  35596  cvmsss2  35625  cvmcov2  35626  cvmopnlem  35629  cvmliftlem14  35648  cvmliftlem15  35649  cvmlift2lem11  35664  cvmlift2lem12  35665  cvmlift2lem13  35666  cvmlift3lem2  35671  cvmlift3lem6  35675  cvmlift3lem9  35678  mthmi  35928  r1peuqusdeg1  35994  br8  36107  br6  36108  br4  36109  dfon2lem9  36140  wzel  36173  wsuclem  36174  wsuclb  36177  imagesset  36304  fvtransport  36383  brcolinear  36410  brsegle  36459  seglerflx  36463  seglemin  36464  btwnsegle  36468  fvray  36492  fvline  36495  hilbert1.1  36505  elhf2  36526  0hf  36528  nn0prpwlem  36683  nn0prpw  36684  fness  36710  fneref  36711  fnessref  36718  refssfne  36719  neibastop2lem  36721  fnemeet1  36727  tailfb  36738  filnetlem4  36742  limsucncmpi  36806  ttctr  36854  dfttc2g  36867  taupilemrplb  37813  qdiff  37820  relowlssretop  37858  rdgellim  37871  matunitlindflem2  38117  ptrecube  38120  poimirlem4  38124  poimirlem17  38137  poimirlem20  38140  poimirlem23  38143  poimirlem24  38144  poimirlem26  38146  poimirlem27  38147  poimirlem29  38149  poimirlem32  38152  heicant  38155  mblfinlem1  38157  mblfinlem2  38158  mblfinlem3  38159  mblfinlem4  38160  ismblfin  38161  volsupnfl  38165  itg2addnclem  38171  itg2addnclem3  38173  itg2addnc  38174  ftc1anclem5  38197  unirep  38214  cover2  38215  indexa  38233  frinfm  38235  sdclem1  38243  fdc  38245  incsequz  38248  caushft  38261  istotbnd3  38271  0totbnd  38273  sstotbnd2  38274  sstotbnd  38275  sstotbnd3  38276  isbnd3  38284  ssbnd  38288  equivbnd  38290  prdsbnd  38293  prdstotbnd  38294  cntotbnd  38296  heibor1lem  38309  heiborlem1  38311  heiborlem3  38313  heiborlem6  38316  heiborlem8  38318  bfplem2  38323  rrncmslem  38332  iccbnd  38340  opidonOLD  38352  exidres  38378  isrngod  38398  isgrpda  38455  isdrngo2  38458  igenval  38561  igenidl  38563  prtlem10  39490  lshpnel2N  39610  lsmsat  39633  lssatomic  39636  lcvnbtwn  39650  lfl1  39695  eqlkr  39724  lshpkrlem1  39735  lshpkrex  39743  cvrcon3b  39902  cvrat4  40068  3dim3  40094  ps-2  40103  llni  40133  llnle  40143  lplni  40157  lplnle  40165  lplnexllnN  40189  lvoli  40200  lnatexN  40404  elpaddn0  40425  pclfinN  40525  lhprelat3N  40665  4atexlemex2  40696  4atex  40701  4atex2-0aOLDN  40703  4atex2-0cOLDN  40705  lautcvr  40717  cdleme0ex1N  40848  cdleme50rnlem  41169  cdleme50ex  41184  cdlemg1cex  41213  cdlemkid5  41560  cdlemk  41599  tendoex  41600  cdleml5N  41605  cdlemm10N  41743  dih1dimatlem0  41953  dihjat1lem  42053  dvh3dim2  42073  dvh3dim3N  42074  dochkr1  42103  dochkr1OLDN  42104  lcfrvalsnN  42166  lcfrlem27  42194  lcfrlem37  42204  lcfr  42210  mapd1o  42273  mapdpglem23  42319  hdmap11lem2  42467  primrootsunit1  42715  zdivgd  42947  resubeu  42987  fidomncyc  43154  nacsfix  43294  mzpcompact2lem  43333  eldioph  43340  diophrw  43341  diophin  43354  rexrabdioph  43372  rexzrexnn0  43382  eldioph4b  43389  rencldnfilem  43398  irrapxlem5  43404  irrapxlem6  43405  pell1234qrdich  43439  pell14qrdich  43447  infmrgelbi  43456  pellqrex  43457  pellfundre  43459  pellfundlb  43462  rmxynorm  43496  congrep  43551  acongrep  43558  jm2.27  43586  fnwe2lem2  43629  islssfgi  43650  hbtlem2  43702  hbtlem4  43704  hbtlem5  43706  dgraaub  43726  mpaaeu  43728  aaitgo  43740  unielss  43796  onexgt  43818  onexomgt  43819  onexlimgt  43821  onexoegt  43822  oaordnr  43874  omnord1  43883  oenord1  43894  oaomoencom  43895  oenass  43897  tfsconcatfv2  43918  tfsconcatrn  43920  tfsconcatb0  43922  ofoafo  43934  naddcnffo  43942  oaun3lem1  43952  naddwordnexlem4  43979  sucomisnotcard  44121  clsk1independent  44623  0elaxnul  45560  pwclaxpow  45561  prclaxpr  45562  uniclaxun  45563  omssaxinf2  45565  wfac8prim  45579  restuni3  45697  iinssd  45710  founiiun  45758  wessf1ornlem  45764  founiiun0  45769  unirnmap  45785  dstregt0  45862  uzfissfz  45903  rpgtrecnn  45956  rexabslelem  45993  infrnmptle  45998  infxrunb3rnmpt  46003  infxrpnf  46021  supminfxr  46039  rexanuz2nf  46067  iooiinicc  46119  iooiinioc  46133  uzubioo  46142  climsuse  46185  islptre  46196  limsuppnfdlem  46276  climinf3  46291  limsupmnfuzlem  46301  limsupre3lem  46307  limsupre3uzlem  46310  0cnv  46317  liminfreuzlem  46377  cnrefiisplem  46404  icccncfext  46462  cncficcgt0  46463  dvbdfbdioo  46505  ioodvbdlimc1lem1  46506  ioodvbdlimc1lem2  46507  ioodvbdlimc2lem  46509  stoweidlem9  46584  stoweidlem14  46589  stoweidlem18  46593  stoweidlem21  46596  stoweidlem29  46604  stoweidlem34  46609  stoweidlem35  46610  stoweidlem39  46614  stoweidlem41  46616  stoweidlem45  46620  stoweidlem52  46627  stoweidlem55  46630  stoweidlem57  46632  stoweidlem60  46635  stirlinglem5  46653  stirlinglem13  46661  stirlinglem14  46662  fourierdlem16  46698  fourierdlem20  46702  fourierdlem21  46703  fourierdlem22  46704  fourierdlem25  46707  fourierdlem31  46713  fourierdlem39  46721  fourierdlem41  46723  fourierdlem42  46724  fourierdlem47  46728  fourierdlem48  46729  fourierdlem51  46732  fourierdlem63  46744  fourierdlem64  46745  fourierdlem65  46746  fourierdlem77  46758  fourierdlem81  46762  fourierdlem83  46764  fourierdlem103  46784  fourierdlem104  46785  elaa2lem  46808  etransclem47  46856  qndenserrnbl  46870  ioorrnopnlem  46879  ioorrnopnxrlem  46881  intsaluni  46904  salgencntex  46918  subsaliuncllem  46932  sge0resplit  46981  sge0seq  47021  sge0reuz  47022  nnfoctbdjlem  47030  meaiininclem  47061  hoicvrrex  47131  ovnlecvr  47133  ovnlerp  47137  hoidmv1lelem2  47167  hoidmvlelem2  47171  hoidmvlelem3  47172  ovnhoilem1  47176  ovnlecvr2  47185  hoiqssbl  47200  ovolval4lem2  47225  ovolval5lem2  47228  ovnovollem1  47231  ovnovollem2  47232  iinhoiicclem  47248  smfinflem  47392  smflimsuplem7  47401  nthrucw  47463  sprsymrelfolem2  48100  perfectALTV  48346  9gbo  48397  11gbo  48398  nnsum3primes4  48411  nnsum3primesprm  48413  ssnn0ssfz  48972  lincsumcl  49054  lincscmcl  49055  zlmodzxzldep  49127  ldepsnlinc  49131  line2ylem  49374  line2xlem  49376  sepfsepc  49550  lubsscl  49582  glbsscl  49583  nelsubc3lem  49692  cnelsubclem  50225  aacllem  50423