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  17587  mreexexlem4d  17588  iscatd  17614  cat1  18039  poslubd  18352  fpwipodrs  18481  ismgmid2  18577  mgmidsssn0  18581  gsumval2a  18594  ismndd  18665  isgrpd2  18870  isgrpd  18872  imasgrp2  18969  mhmmnd  18978  ghmgrp  18980  gaorber  19222  orbsta  19227  cayleyth  19329  pmtrdifel  19394  pmtrdifwrdel  19399  pmtrdifwrdel2  19400  psgnunilem2  19409  psgnunilem3  19410  psgnvalii  19423  pgpfi1  19509  sylow1lem3  19514  sylow1lem5  19516  pgpfi  19519  sylow2alem2  19532  efgredeu  19666  lt6abl  19809  pgpfac1lem3a  19992  pgpfac1lem3  19993  pgpfac1lem5  19995  pgpfaclem1  19997  pgpfaclem3  19999  ablfaclem2  20002  dvdsrmul  20284  dvdsr01  20291  irredrmul  20347  rhmdvdsr  20428  rgspnval  20532  rgspncl  20533  lspf  20912  lspval  20913  lssats2  20938  lspfixed  21070  lspsolvlem  21084  zringlpir  21409  pzriprnglem13  21435  zncyg  21490  cygth  21513  frlmup4  21743  aspval  21815  evlseu  22023  fiinbas  22872  topbas  22892  pptbas  22928  clsval  22957  elcls  22993  neiint  23024  neips  23033  opnneissb  23034  opnssneib  23035  innei  23045  neiptopnei  23052  restbas  23078  neitr  23100  pnfnei  23140  mnfnei  23141  lmconst  23181  iscnp4  23183  cncnpi  23198  cnconst2  23203  cnprest  23209  cnpdis  23213  nrmsep  23277  regsep2  23296  cmpcovf  23311  cmpsub  23320  cmpcld  23322  hauscmplem  23326  conncompid  23351  2ndci  23368  2ndcsb  23369  2ndc1stc  23371  1stcrest  23373  2ndcctbss  23375  2ndcdisj  23376  2ndcomap  23378  2ndcsep  23379  dis2ndc  23380  restlly  23403  islly2  23404  hausllycmp  23414  cldllycmp  23415  lly1stc  23416  dislly  23417  ssref  23432  refref  23433  finlocfin  23440  dissnlocfin  23449  locfindis  23450  llycmpkgen2  23470  cmpkgen  23471  1stckgenlem  23473  elptr  23493  ptbasfi  23501  neitx  23527  ptpjopn  23532  txcnp  23540  ptcnplem  23541  txlly  23556  txnlly  23557  txtube  23560  txcmplem1  23561  tx1stc  23570  txkgen  23572  xkococnlem  23579  txconn  23609  tgqtop  23632  kqreglem1  23661  kqreglem2  23662  kqnrmlem1  23663  kqnrmlem2  23664  reghmph  23713  nrmhmph  23714  fbssfi  23757  opnfbas  23762  isfil2  23776  fsubbas  23787  ssfg  23792  fgss2  23794  fbasrn  23804  filuni  23805  fgtr  23810  ssufl  23838  uffix  23841  elfm2  23868  elfm3  23870  imaelfm  23871  rnelfmlem  23872  rnelfm  23873  fmfnfmlem4  23877  fmfnfm  23878  fmco  23881  ufldom  23882  hausflim  23901  flimcls  23905  hauspwpwf1  23907  flffbas  23915  txflf  23926  fclscf  23945  fclsfnflim  23947  alexsubALTlem4  23970  alexsubALT  23971  tmdgsum2  24016  symgtgp  24026  subgntr  24027  opnsubg  24028  ghmcnp  24035  qustgpopn  24040  tsmsfbas  24048  tsmsxplem1  24073  ustexsym  24136  trust  24150  utoptop  24155  restutop  24158  restutopopn  24159  ustuqtop4  24165  utopsnneiplem  24168  iducn  24203  fmucnd  24212  cfilufg  24213  trcfilu  24214  neipcfilu  24216  imasdsf1olem  24294  blssps  24345  blss  24346  blssexps  24347  blssex  24348  ssblex  24349  blin2  24350  neibl  24422  blcld  24426  metss2  24433  stdbdmopn  24439  met1stc  24442  met2ndci  24443  metrest  24445  prdsxmslem2  24450  metcnp3  24461  metustexhalf  24477  metustfbas  24478  cfilucfil  24480  restmetu  24491  dscopn  24494  ngptgp  24557  nlmvscnlem1  24607  tgioo  24717  tgqioo  24721  xrsmopn  24734  zcld  24735  recld2  24736  zdis  24738  icccmplem1  24744  icccmplem2  24745  xmetdcn2  24759  addcnlem  24786  xrhmeo  24877  cnheibor  24887  cnllycmp  24888  lebnumlem3  24895  lebnum  24896  xlebnum  24897  lebnumii  24898  elpi1i  24979  ipcnlem1  25178  lmnn  25196  iscfil3  25206  cfilres  25229  flimcfil  25247  bcthlem4  25260  bcthlem5  25261  minveclem4c  25358  minveclem2  25359  minveclem3b  25361  minveclem3  25362  minveclem4  25365  minveclem6  25367  ivthlem2  25386  ivth  25388  ivthle  25390  ivthle2  25391  elovolmr  25410  ovolunlem1  25431  ovoliunlem2  25437  ovolicc1  25450  iundisj  25482  iunmbl2  25491  dyadmbllem  25533  volivth  25541  mbflimsup  25600  i1faddlem  25627  i1fmullem  25628  itg2lr  25664  itg2monolem1  25684  limcnlp  25812  ellimc3  25813  limcflf  25815  limciun  25828  rollelem  25926  c1lip1  25935  lhop1lem  25951  ply1divex  26075  ig1peu  26113  elply2  26134  coeeq  26165  plydivlem3  26236  plydivlem4  26237  elqaalem3  26262  qaa  26264  iaa  26266  aareccl  26267  aannenlem2  26270  aalioulem2  26274  aalioulem3  26275  aalioulem5  26277  aalioulem6  26278  aaliou  26279  aaliou2  26281  aaliou3lem8  26286  ulmshftlem  26331  reeff1o  26390  pilem2  26395  pilem3  26396  efif1olem2  26485  efopn  26600  cxpcn3lem  26690  cxpeq  26700  dcubic2  26787  quart  26804  xrlimcnp  26911  ftalem5  27020  ftalem7  27022  sgmnncl  27090  dvdsppwf1o  27129  musum  27134  perfect  27175  dchrptlem1  27208  dchrptlem2  27209  dchrpt  27211  bpos1lem  27226  lgsqrlem4  27293  lgsdchrval  27298  2sqblem  27375  dchrisumlem3  27435  chpdifbndlem2  27498  pntrsumbnd2  27511  pntpbnd1  27530  pntpbnd2  27531  pntpbnd  27532  pntibndlem2  27535  pntibndlem3  27536  pntleme  27552  pntlem3  27553  elno2  27599  sltval2  27601  noreson  27605  sltres  27607  noseponlem  27609  nolesgn2o  27616  nogesgn1o  27618  nodense  27637  nosupfv  27651  nosupres  27652  nosupbnd1lem3  27655  nosupbnd1lem5  27657  nosupbnd2lem1  27660  noinffv  27666  noinfres  27667  noinfbnd1lem3  27670  noinfbnd1lem5  27672  noinfbnd2lem1  27675  noetasuplem4  27681  noetainflem4  27685  noetalem2  27687  cuteq0  27781  cuteq1  27783  oldlim  27836  bdayiun  27864  cofcutrtime  27875  cofss  27878  coiniss  27879  cutlt  27880  cutmax  27882  cutmin  27883  negsex  27989  negsfo  27999  norecdiv  28133  divs1  28147  precsexlem11  28159  precsex  28160  recsex  28161  elons2d  28200  onscutlt  28205  n0ons  28268  bdayn0sf1o  28299  dfnns2  28301  zsoring  28336  pw2recs  28365  halfcut  28381  0reno  28401  readdscl  28403  axtgcont  28449  tgcgrxfr  28498  legid  28567  btwnleg  28568  leg0  28572  tghilberti1  28617  tglnpt2  28621  colline  28629  mirreu3  28634  isperp2  28695  colperpex  28713  lnopp2hpgb  28743  hpgerlem  28745  brbtwn  28879  brcgr  28880  brbtwn2  28885  axpasch  28921  axlowdimlem14  28935  axlowdim2  28940  axcontlem2  28945  axcontlem4  28947  axcontlem8  28951  axcontlem10  28953  axcontlem12  28955  fusgrn0degnn0  29480  friendshipgt3  30377  lpni  30459  isgrpoi  30477  vacn  30673  smcnlem  30676  nmosetn0  30744  nmoolb  30750  nmobndi  30754  nmoo0  30770  nmlno0lem  30772  isblo3i  30780  blo3i  30781  blocnilem  30783  ubthlem1  30849  minvecolem2  30854  minvecolem3  30855  minvecolem4c  30858  minvecolem4  30859  minvecolem5  30860  minvecolem6  30861  norm1exi  31229  occl  31283  spanval  31312  spancl  31315  shsval2i  31366  ococin  31387  pjoml6i  31568  nmopsetn0  31844  nmfnsetn0  31857  nmoplb  31886  nmfnlb  31903  nmop0  31965  nmfn0  31966  nmlnop0iALT  31974  nmopun  31993  nmcexi  32005  lnconi  32012  lnopcnbd  32015  lnfncnbd  32036  riesz3i  32041  riesz1  32044  cnlnadjlem2  32047  cnlnadjlem8  32053  cnlnadjlem9  32054  adjbd1o  32064  branmfn  32084  opsqrlem1  32119  pjnmopi  32127  strlem1  32229  stri  32236  hstri  32244  cvcon3  32263  cvnbtwn  32265  superpos  32333  shatomici  32337  atcvat4i  32376  mdsymlem2  32383  cdj1i  32412  cdj3i  32420  rexunirn  32471  foresf1o  32483  iundisjf  32568  aciunf1lem  32636  fnpreimac  32645  fgreu  32646  fcnvgreu  32647  xrge0infss  32733  ssnnssfz  32760  iundisjfi  32769  indf1ofs  32839  xreceu  32892  rexdiv  32896  isarchi3  33156  archirngz  33158  archiabllem2a  33163  0nellinds  33334  qtophaus  33819  reff  33822  locfinreflem  33823  cmpcref  33833  dispcmp  33842  tpr2rico  33895  pnfneige0  33934  qqhucn  33975  rrhre  34004  esumcst  34046  esumpcvgval  34061  dmsigagen  34127  rossros  34163  dya2icoseg  34261  dya2iocnrect  34265  dya2iocuni  34267  eulerpartlemgvv  34360  dstfrvunirn  34459  ballotlem4  34483  ballotlemic  34491  ballotlem1c  34492  ballotlemrc  34515  signsw0g  34540  signswmnd  34541  prodfzo03  34587  tgoldbachgt  34647  onvf1odlem4  35086  loop1cycl  35117  umgr2cycllem  35120  umgr2cycl  35121  subfacp1lem3  35162  erdsze2lem2  35184  cnpconn  35210  txpconn  35212  ptpconn  35213  indispconn  35214  connpconn  35215  cvxpconn  35222  cnllysconn  35225  cvmsss2  35254  cvmcov2  35255  cvmopnlem  35258  cvmliftlem14  35277  cvmliftlem15  35278  cvmlift2lem11  35293  cvmlift2lem12  35294  cvmlift2lem13  35295  cvmlift3lem2  35300  cvmlift3lem6  35304  cvmlift3lem9  35307  mthmi  35557  r1peuqusdeg1  35623  br8  35736  br6  35737  br4  35738  dfon2lem9  35772  wzel  35805  wsuclem  35806  wsuclb  35809  imagesset  35934  fvtransport  36013  brcolinear  36040  brsegle  36089  seglerflx  36093  seglemin  36094  btwnsegle  36098  fvray  36122  fvline  36125  hilbert1.1  36135  elhf2  36156  0hf  36158  nn0prpwlem  36303  nn0prpw  36304  fness  36330  fneref  36331  fnessref  36338  refssfne  36339  neibastop2lem  36341  fnemeet1  36347  tailfb  36358  filnetlem4  36362  limsucncmpi  36426  taupilemrplb  37301  relowlssretop  37344  rdgellim  37357  matunitlindflem2  37604  ptrecube  37607  poimirlem4  37611  poimirlem17  37624  poimirlem20  37627  poimirlem23  37630  poimirlem24  37631  poimirlem26  37633  poimirlem27  37634  poimirlem29  37636  poimirlem32  37639  heicant  37642  mblfinlem1  37644  mblfinlem2  37645  mblfinlem3  37646  mblfinlem4  37647  ismblfin  37648  volsupnfl  37652  itg2addnclem  37658  itg2addnclem3  37660  itg2addnc  37661  ftc1anclem5  37684  unirep  37701  cover2  37702  indexa  37720  frinfm  37722  sdclem1  37730  fdc  37732  incsequz  37735  caushft  37748  istotbnd3  37758  0totbnd  37760  sstotbnd2  37761  sstotbnd  37762  sstotbnd3  37763  isbnd3  37771  ssbnd  37775  equivbnd  37777  prdsbnd  37780  prdstotbnd  37781  cntotbnd  37783  heibor1lem  37796  heiborlem1  37798  heiborlem3  37800  heiborlem6  37803  heiborlem8  37805  bfplem2  37810  rrncmslem  37819  iccbnd  37827  opidonOLD  37839  exidres  37865  isrngod  37885  isgrpda  37942  isdrngo2  37945  igenval  38048  igenidl  38050  prtlem10  38851  lshpnel2N  38971  lsmsat  38994  lssatomic  38997  lcvnbtwn  39011  lfl1  39056  eqlkr  39085  lshpkrlem1  39096  lshpkrex  39104  cvrcon3b  39263  cvrat4  39430  3dim3  39456  ps-2  39465  llni  39495  llnle  39505  lplni  39519  lplnle  39527  lplnexllnN  39551  lvoli  39562  lnatexN  39766  elpaddn0  39787  pclfinN  39887  lhprelat3N  40027  4atexlemex2  40058  4atex  40063  4atex2-0aOLDN  40065  4atex2-0cOLDN  40067  lautcvr  40079  cdleme0ex1N  40210  cdleme50rnlem  40531  cdleme50ex  40546  cdlemg1cex  40575  cdlemkid5  40922  cdlemk  40961  tendoex  40962  cdleml5N  40967  cdlemm10N  41105  dih1dimatlem0  41315  dihjat1lem  41415  dvh3dim2  41435  dvh3dim3N  41436  dochkr1  41465  dochkr1OLDN  41466  lcfrvalsnN  41528  lcfrlem27  41556  lcfrlem37  41566  lcfr  41572  mapd1o  41635  mapdpglem23  41681  hdmap11lem2  41829  primrootsunit1  42078  zdivgd  42318  resubeu  42358  fidomncyc  42516  nacsfix  42693  mzpcompact2lem  42732  eldioph  42739  diophrw  42740  diophin  42753  rexrabdioph  42775  rexzrexnn0  42785  eldioph4b  42792  rencldnfilem  42801  irrapxlem5  42807  irrapxlem6  42808  pell1234qrdich  42842  pell14qrdich  42850  infmrgelbi  42859  pellqrex  42860  pellfundre  42862  pellfundlb  42865  rmxynorm  42900  congrep  42955  acongrep  42962  jm2.27  42990  fnwe2lem2  43033  islssfgi  43054  hbtlem2  43106  hbtlem4  43108  hbtlem5  43110  dgraaub  43130  mpaaeu  43132  aaitgo  43144  unielss  43200  onexgt  43222  onexomgt  43223  onexlimgt  43225  onexoegt  43226  oaordnr  43278  omnord1  43287  oenord1  43298  oaomoencom  43299  oenass  43301  tfsconcatfv2  43322  tfsconcatrn  43324  tfsconcatb0  43326  ofoafo  43338  naddcnffo  43346  oaun3lem1  43356  naddwordnexlem4  43383  sucomisnotcard  43526  clsk1independent  44028  0elaxnul  44966  pwclaxpow  44967  prclaxpr  44968  uniclaxun  44969  omssaxinf2  44971  wfac8prim  44985  restuni3  45105  iinssd  45118  founiiun  45166  wessf1ornlem  45172  founiiun0  45177  unirnmap  45195  dstregt0  45273  uzfissfz  45315  rpgtrecnn  45369  rexabslelem  45407  infrnmptle  45412  infxrunb3rnmpt  45417  infxrpnf  45435  supminfxr  45453  rexanuz2nf  45481  iooiinicc  45533  iooiinioc  45547  uzubioo  45556  climsuse  45599  islptre  45610  limsuppnfdlem  45692  climinf3  45707  limsupmnfuzlem  45717  limsupre3lem  45723  limsupre3uzlem  45726  0cnv  45733  liminfreuzlem  45793  cnrefiisplem  45820  icccncfext  45878  cncficcgt0  45879  dvbdfbdioo  45921  ioodvbdlimc1lem1  45922  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  stoweidlem9  46000  stoweidlem14  46005  stoweidlem18  46009  stoweidlem21  46012  stoweidlem29  46020  stoweidlem34  46025  stoweidlem35  46026  stoweidlem39  46030  stoweidlem41  46032  stoweidlem45  46036  stoweidlem52  46043  stoweidlem55  46046  stoweidlem57  46048  stoweidlem60  46051  stirlinglem5  46069  stirlinglem13  46077  stirlinglem14  46078  fourierdlem16  46114  fourierdlem20  46118  fourierdlem21  46119  fourierdlem22  46120  fourierdlem25  46123  fourierdlem31  46129  fourierdlem39  46137  fourierdlem41  46139  fourierdlem42  46140  fourierdlem47  46144  fourierdlem48  46145  fourierdlem49  46146  fourierdlem51  46148  fourierdlem63  46160  fourierdlem64  46161  fourierdlem65  46162  fourierdlem77  46174  fourierdlem81  46178  fourierdlem83  46180  fourierdlem103  46200  fourierdlem104  46201  elaa2lem  46224  etransclem47  46272  qndenserrnbl  46286  ioorrnopnlem  46295  ioorrnopnxrlem  46297  intsaluni  46320  salgencntex  46334  subsaliuncllem  46348  sge0resplit  46397  sge0seq  46437  sge0reuz  46438  nnfoctbdjlem  46446  meaiininclem  46477  hoicvrrex  46547  ovnlecvr  46549  ovnlerp  46553  hoidmv1lelem2  46583  hoidmvlelem2  46587  hoidmvlelem3  46588  ovnhoilem1  46592  ovnlecvr2  46601  hoiqssbl  46616  ovolval4lem2  46641  ovolval5lem2  46644  ovnovollem1  46647  ovnovollem2  46648  iinhoiicclem  46664  smfinflem  46808  smflimsuplem7  46817  sprsymrelfolem2  47487  perfectALTV  47717  9gbo  47768  11gbo  47769  nnsum3primes4  47782  nnsum3primesprm  47784  ssnn0ssfz  48330  lincsumcl  48413  lincscmcl  48414  zlmodzxzldep  48486  ldepsnlinc  48490  line2ylem  48733  line2xlem  48735  sepfsepc  48909  lubsscl  48941  glbsscl  48942  nelsubc3lem  49052  cnelsubclem  49585  aacllem  49783