Theorem rspcev 3580

Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2179, ax-11 2196, ax-12 2215. (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 3573	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝜓 → ∃𝑥 ∈ 𝐵 𝜑))
5	4	imp 412	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2146  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091

This theorem is used by:  rspcedvdw  3583  rspceaimv  3586  rspc2ev  3592  rspc3ev  3596  rspceeqv  3602  reu6i  3689  rspesbca  3832  eliuni  4960  iuneqconst  4966  brralrspcev  5168  wefrc  5649  wereu2  5652  xpdifid  6165  xpdifcnvepel  6166  frpomin  6350  onfr  6409  onelssex  6419  ordunidif  6420  eliman0  6933  dffv2  6991  elrnrexdm  7100  eldmrexrn  7102  elabrex  7256  elabrexg  7257  f1elima  7277  fliftfun  7330  fliftval  7334  f1oiso2  7370  sorpssuni  7758  sorpssint  7759  onssmin  7816  onminex  7826  fimaproj  8165  frxp3  8181  poseq  8188  tfrlem12  8411  seqomlem2  8475  oawordeulem  8576  oaass  8583  odi  8601  omass  8602  omeulem1  8604  oen0  8609  oelim2  8618  oeeulem  8624  nnawordex  8660  nnaordex2  8662  eldifsucnn  8687  cofon1  8695  cofon2  8696  naddcllem  8699  naddunif  8717  boxcutc  8983  0fi  9084  snfi  9085  rexdif1en  9190  findcard  9193  nnfi  9197  pssnn  9198  unfi  9200  onfin  9244  dif1ennnALT  9282  frfi  9290  fisupg  9293  nnsdomg  9305  pwfir  9322  prfi  9329  fissuni  9360  fipreima  9361  finsschain  9362  indexfi  9363  marypha1lem  9438  eqsup  9461  supmax  9473  fisup2g  9474  fisupcl  9475  supisoex  9480  infmin  9501  fiinfg  9506  fiinf2g  9507  wofib  9552  wemaplem2  9554  card2inf  9562  brwdom2  9580  cnfcom3clem  9719  ssttrcl  9729  ttrcltr  9730  trcl  9742  frmin  9766  r1ordg  9798  r1pwss  9804  tz9.12lem3  9809  tz9.12  9810  r1elwf  9817  tcrank  9914  elhf2  9923  0hf  9930  scottex  9946  scottexOLD  9947  scott0b  9950  scott0OLD  9951  isnumi  10040  onsdom  10090  ondomen  10129  infpwfien  10154  cardaleph  10181  infenaleph  10183  alephfplem4  10199  alephfp2  10201  dfac2b  10222  ackbij1lem18  10327  ackbij1  10328  cflem  10336  cflecard  10343  cfsuc  10348  cfflb  10350  cofsmo  10360  coftr  10364  fin23lem7  10407  fin23lem11  10408  enfin2i  10412  fin23lem26  10416  isf32lem5  10448  isf34lem4  10468  isfin1-3  10477  fin1a2lem7  10497  axdc3lem4  10544  ttukeylem7  10606  iunfo  10636  ficard  10662  pwcfsdom  10681  fpwwe2lem11  10739  wunex  10837  eltsk2g  10849  grur1  10918  axgroth6  10926  inaprc  10934  nqereu  11027  archnq  11078  genpnmax  11105  ltexpri  11141  prlem936  11145  recexpr  11149  supexpr  11152  negexsr  11200  recexsrlem  11201  recexsr  11205  supsrlem  11209  axrnegex  11260  axrrecex  11261  axpre-sup  11267  1re  11321  dedekind  11486  dedekindle  11487  cnegex  11504  cnegex2  11505  recex  11961  receu  11974  fiminre2  12278  cju  12329  nn2ge  12378  nominpos  12596  zdiv  12782  btwnz  12815  uzwo  13051  ublbneg  13073  lbzbi  13076  zsupss  13077  uzsupss  13080  rpnnen1lem1  13119  rpnnen1lem3  13120  rpnnen1lem4  13121  rpnnen1lem5  13122  z2ge  13341  qbtwnre  13342  qbtwnxr  13343  xralrple  13348  xrsupsslem  13450  xrinfmsslem  13451  supxrpnf  13461  icc0  13537  uzsup  14016  expnbnd  14389  expmulnbnd  14392  hashkf  14489  hashdom  14536  iswrdi  14675  rtrclreclem1  15225  rtrclreclem2  15227  rtrclreclem3  15228  01sqrex  15431  resqrex  15432  sqrtneg  15449  abs1m  15518  rexanuz  15528  rexuz3  15531  rexuzre  15535  sqreu  15543  o1lo1  15719  climconst  15725  rlimclim1  15727  climshftlem  15756  rlimo1  15799  lo1add  15809  lo1mul  15810  lo1le  15834  isercoll  15850  serf0  15863  zsum  15899  fsum  15901  fsumcvg3  15910  mertenslem1  16068  ntrivcvgn0  16082  ntrivcvgmullem  16085  zprod  16119  fprod  16123  fprodntriv  16124  dvdsval2  16440  dvds0lem  16451  dvds1lem  16452  dvds2lem  16453  odd2np1lem  16525  odd2np1  16526  opeo  16550  omeo  16551  divalglem9  16586  gcdcllem3  16686  lcmcllem  16786  qredeu  16848  exprmfct  16895  isprm5  16898  odzcllem  16985  reumodprminv  16997  modprm0  16998  nnnn0modprm0  16999  pythagtriplem19  17026  pcprmpw2  17075  pockthi  17100  infpnlem2  17104  vdwlem2  17175  vdwlem10  17183  vdwlem13  17186  ramub1lem1  17219  cshwrepswhash1  17295  imasleval  17728  mreexexlem3d  17835  mreexexlem4d  17836  iscatd  17862  cat1  18287  poslubd  18600  fpwipodrs  18729  ismgmid2  18864  mgmidsssn0  18868  mgmidpfod  18872  gsumval2a  18889  ismndd  18961  isgrpd2  19182  isgrpd  19184  imasgrp2  19280  mhmmnd  19289  ghmgrp  19291  gaorber  19537  orbsta  19542  cayleyth  19644  pmtrdifel  19709  pmtrdifwrdel  19714  pmtrdifwrdel2  19715  psgnunilem2  19724  psgnunilem3  19725  psgnvalii  19738  pgpfi1  19824  sylow1lem3  19829  sylow1lem5  19831  pgpfi  19834  sylow2alem2  19847  efgredeu  19981  lt6abl  20124  pgpfac1lem3a  20307  pgpfac1lem3  20308  pgpfac1lem5  20310  pgpfaclem1  20312  pgpfaclem3  20314  ablfaclem2  20317  dvdsrmul  20609  dvdsr01  20616  irredrmul  20672  rhmdvdsr  20773  rgspnval  20879  rgspncl  20880  lspf  21264  lspval  21265  lssats2  21290  lspfixed  21421  lspsolvlem  21435  zringlpir  21788  pzriprnglem13  21814  zncyg  21869  cygth  21892  frlmup4  22122  aspval  22195  evlseu  22407  matunitlindflem2  23010  fiinbas  23285  topbas  23305  pptbas  23341  clsval  23370  elcls  23406  neiint  23437  neips  23446  opnneissb  23447  opnssneib  23448  innei  23458  neiptopnei  23465  restbas  23491  neitr  23513  pnfnei  23553  mnfnei  23554  lmconst  23594  iscnp4  23596  cncnpi  23611  cnconst2  23616  cnprest  23622  cnpdis  23626  nrmsep  23690  regsep2  23709  cmpcovf  23724  cmpsub  23733  cmpcld  23735  hauscmplem  23739  conncompid  23764  2ndci  23781  2ndcsb  23782  2ndc1stc  23784  1stcrest  23786  2ndcctbss  23789  2ndcdisj  23790  2ndcomap  23792  2ndcsep  23793  dis2ndc  23794  restlly  23817  islly2  23818  hausllycmp  23828  cldllycmp  23829  lly1stc  23830  dislly  23831  ssref  23846  refref  23847  finlocfin  23854  dissnlocfin  23863  locfindis  23864  llycmpkgen2  23884  cmpkgen  23885  1stckgenlem  23887  elptr  23907  ptbasfi  23915  neitx  23941  ptpjopn  23946  txcnp  23954  ptcnplem  23955  txlly  23970  txnlly  23971  txtube  23974  txcmplem1  23975  tx1stc  23984  txkgen  23986  xkococnlem  23993  txconn  24023  tgqtop  24046  kqreglem1  24075  kqreglem2  24076  kqnrmlem1  24077  kqnrmlem2  24078  reghmph  24127  nrmhmph  24128  fbssfi  24171  opnfbas  24176  isfil2  24190  fsubbas  24201  ssfg  24206  fgss2  24208  fbasrn  24218  filuni  24219  fgtr  24224  ssufl  24252  uffix  24255  elfm2  24282  elfm3  24284  imaelfm  24285  rnelfmlem  24286  rnelfm  24287  fmfnfmlem4  24291  fmfnfm  24292  fmco  24295  ufldom  24296  hausflim  24315  flimcls  24319  hauspwpwf1  24321  flffbas  24329  txflf  24340  fclscf  24359  fclsfnflim  24361  alexsubALTlem4  24384  alexsubALT  24385  tmdgsum2  24430  symgtgp  24440  subgntr  24441  opnsubg  24442  ghmcnp  24449  qustgpopn  24454  tsmsfbas  24462  tsmsxplem1  24487  ustexsym  24550  trust  24563  utoptop  24568  restutop  24571  restutopopn  24572  ustuqtop4  24578  utopsnneiplem  24581  iducn  24616  fmucnd  24625  cfilufg  24626  trcfilu  24627  neipcfilu  24629  imasdsf1olem  24707  blssps  24758  blss  24759  blssexps  24760  blssex  24761  ssblex  24762  blin2  24763  neibl  24835  blcld  24839  metss2  24846  stdbdmopn  24852  met1stc  24855  met2ndci  24856  metrest  24858  prdsxmslem2  24863  metcnp3  24874  metustexhalf  24890  metustfbas  24891  cfilucfil  24893  restmetu  24904  dscopn  24907  ngptgp  24970  nlmvscnlem1  25020  tgioo  25130  tgqioo  25134  xrsmopn  25147  zcld  25148  recld2  25149  zdis  25151  icccmplem1  25157  icccmplem2  25158  xmetdcn2  25172  addcnlem  25199  xrhmeo  25282  cnheibor  25291  cnllycmp  25292  lebnumlem3  25299  lebnum  25300  xlebnum  25301  lebnumii  25302  elpi1i  25382  ipcnlem1  25581  lmnn  25599  iscfil3  25609  cfilres  25632  flimcfil  25650  bcthlem4  25663  bcthlem5  25664  minveclem4c  25761  minveclem2  25762  minveclem3b  25764  minveclem3  25765  minveclem4  25768  minveclem6  25770  ivthlem2  25788  ivth  25790  ivthle  25792  ivthle2  25793  elovolmr  25812  ovolunlem1  25833  ovoliunlem2  25839  ovolicc1  25852  iundisj  25884  iunmbl2  25893  dyadmbllem  25935  volivth  25943  mbflimsup  26002  i1faddlem  26029  i1fmullem  26030  itg2lr  26066  itg2monolem1  26086  limcnlp  26213  ellimc3  26214  limcflf  26216  limciun  26229  rollelem  26324  c1lip1  26332  lhop1lem  26348  ply1divex  26470  ig1peu  26508  elply2  26529  coeeq  26561  plydivlem3  26631  plydivlem4  26632  elqaalem3  26659  iaaOLD  26667  aareccl  26668  aannenlem2  26671  aalioulem2  26675  aalioulem3  26676  aalioulem5  26678  aalioulem6  26679  aaliou  26680  aaliou2  26682  aaliou3lem8  26687  ulmshftlem  26731  reeff1o  26789  pilem2  26794  pilem3  26795  efif1olem2  26886  efopn  27001  cxpcn3lem  27090  cxpeq  27100  dcubic2  27187  quart  27204  xrlimcnp  27311  ftalem5  27419  ftalem7  27421  sgmnncl  27489  dvdsppwf1o  27528  musum  27533  perfect  27573  dchrptlem1  27606  dchrptlem2  27607  dchrpt  27609  bpos1lem  27624  lgsqrlem4  27691  lgsdchrval  27696  2sqblem  27773  dchrisumlem3  27833  chpdifbndlem2  27896  pntrsumbnd2  27909  pntpbnd1  27928  pntpbnd2  27929  pntpbnd  27930  pntibndlem2  27933  pntibndlem3  27934  pntleme  27950  pntlem3  27951  elno2  28026  ltsval2  28028  noreson  28032  ltsres  28034  noseponlem  28036  nolesgn2o  28043  nogesgn1o  28045  nodense  28064  nosupfv  28078  nosupres  28079  nosupbnd1lem3  28082  nosupbnd1lem5  28084  nosupbnd2lem1  28087  noinffv  28093  noinfres  28094  noinfbnd1lem3  28097  noinfbnd1lem5  28099  noinfbnd2lem1  28102  noetasuplem4  28108  noetainflem4  28112  noetalem2  28114  cuteq0  28216  cuteq1  28218  oldlim  28288  bdayiun  28316  cofcutrtime  28328  cofss  28331  coiniss  28332  cutlt  28333  cutmax  28335  cutmin  28336  negsex  28444  negsfo  28454  norecdiv  28591  divs1  28605  precsexlem11  28618  precsex  28619  recsex  28620  elons2d  28660  oncutlt  28665  n0on  28737  bdayn0sf1o  28771  dfnns2  28773  zsoring  28810  pw2recs  28839  halfcut  28859  0reno  28897  1reno  28898  readdscl  28900  axtgcont  28946  tgcgrxfr  28996  legid  29065  btwnleg  29066  leg0  29070  tghilberti1  29120  colline  29133  mirreu3  29141  isperp2  29205  colperpex  29224  lnopp2hpgb  29256  hpgerlem  29258  brbtwn  29492  brcgr  29493  brbtwn2  29498  axpasch  29534  axlowdimlem14  29548  axlowdim2  29553  axcontlem2  29558  axcontlem4  29560  axcontlem8  29564  axcontlem10  29566  axcontlem12  29568  fusgrn0degnn0  30095  loop1cycl  30759  umgr2cycllem  30761  umgr2cycl  30762  friendshipgt3  31014  lpni  31097  isgrpoi  31115  vacn  31311  smcnlem  31314  nmosetn0  31382  nmoolb  31388  nmobndi  31392  nmoo0  31408  nmlno0lem  31410  isblo3i  31418  blo3i  31419  blocnilem  31421  ubthlem1  31487  minvecolem2  31492  minvecolem3  31493  minvecolem4c  31496  minvecolem4  31497  minvecolem5  31498  minvecolem6  31499  norm1exi  31867  occl  31921  spanval  31950  spancl  31953  shsval2i  32004  ococin  32025  pjoml6i  32206  nmopsetn0  32482  nmfnsetn0  32495  nmoplb  32524  nmfnlb  32541  nmop0  32603  nmfn0  32604  nmlnop0iALT  32612  nmopun  32631  nmcexi  32643  lnconi  32650  lnopcnbd  32653  lnfncnbd  32674  riesz3i  32679  riesz1  32682  cnlnadjlem2  32685  cnlnadjlem8  32691  cnlnadjlem9  32692  adjbd1o  32702  branmfn  32722  opsqrlem1  32757  pjnmopi  32765  strlem1  32867  stri  32874  hstri  32882  cvcon3  32901  cvnbtwn  32903  superpos  32971  shatomici  32975  atcvat4i  33014  mdsymlem2  33021  cdj1i  33050  cdj3i  33058  rexunirn  33145  iundisjf  33240  aciunf1lem  33313  fnpreimac  33321  fgreu  33322  fcnvgreu  33323  xrge0infss  33408  ssnnssfz  33435  iundisjfi  33444  indf1ofs  33489  xreceu  33544  rexdiv  33548  isarchi3  33804  archirngz  33806  archiabllem2a  33811  0nellinds  33982  qtophaus  34524  locfinreflem  34528  dispcmp  34547  tpr2rico  34600  pnfneige0  34639  qqhucn  34680  rrhre  34709  esumcst  34751  esumpcvgval  34766  dmsigagen  34833  rossros  34869  dya2icoseg  34965  dya2iocnrect  34969  dya2iocuni  34971  eulerpartlemgvv  35064  dstfrvunirn  35163  ballotlem4  35187  ballotlemic  35195  ballotlemrc  35219  signsw0g  35241  signswmnd  35242  prodfzo03  35288  tgoldbachgt  35348  rankse  35805  acwer1prclem  35833  onvf1odlem4  35991  subfacp1lem3  36071  erdsze2lem2  36093  cnpconn  36119  txpconn  36121  ptpconn  36122  indispconn  36123  connpconn  36124  cvxpconn  36131  cnllysconn  36134  cvmsss2  36163  cvmcov2  36164  cvmopnlem  36167  cvmliftlem14  36186  cvmliftlem15  36187  cvmlift2lem11  36202  cvmlift2lem12  36203  cvmlift2lem13  36204  cvmlift3lem2  36209  cvmlift3lem6  36213  cvmlift3lem9  36216  mthmi  36466  r1peuqusdeg1  36532  br8  36651  br6  36652  br4  36653  dfon2lem9  36683  wzel  36716  wsuclem  36717  wsuclb  36720  imagesset  36847  fvtransport  36927  brcolinear  36954  brsegle  37003  seglerflx  37007  seglemin  37008  btwnsegle  37012  fvray  37036  fvline  37039  hilbert1.1  37049  nn0prpwlem  37240  nn0prpw  37241  fness  37267  fneref  37268  fnessref  37275  refssfne  37276  neibastop2lem  37278  fnemeet1  37284  tailfb  37295  filnetlem4  37299  limsucncmpi  37363  ttctr  37411  dfttc2g  37424  taupilemrplb  38384  qdiff  38391  relowlssretop  38429  rdgellim  38442  ptrecube  38681  poimirlem4  38685  poimirlem17  38698  poimirlem20  38701  poimirlem23  38704  poimirlem24  38705  poimirlem26  38707  poimirlem27  38708  poimirlem29  38710  poimirlem32  38713  heicant  38716  mblfinlem1  38718  mblfinlem2  38719  mblfinlem3  38720  mblfinlem4  38721  ismblfin  38722  volsupnfl  38726  itg2addnclem  38732  itg2addnclem3  38734  itg2addnc  38735  ftc1anclem5  38758  unirep  38791  cover2  38792  indexa  38810  frinfm  38812  sdclem1  38820  fdc  38822  incsequz  38825  caushft  38838  istotbnd3  38848  0totbnd  38850  sstotbnd2  38851  sstotbnd  38852  sstotbnd3  38853  isbnd3  38861  ssbnd  38865  equivbnd  38867  prdsbnd  38870  prdstotbnd  38871  cntotbnd  38873  heibor1lem  38886  heiborlem1  38888  heiborlem3  38890  heiborlem6  38893  heiborlem8  38895  bfplem2  38900  rrncmslem  38909  iccbnd  38917  opidonOLD  38929  exidres  38955  isrngod  38975  isgrpda  39032  isdrngo2  39035  igenval  39138  igenidl  39140  prtlem10  40065  lshpnel2N  40185  lsmsat  40208  lssatomic  40211  lcvnbtwn  40225  lfl1  40270  eqlkr  40299  lshpkrlem1  40310  lshpkrex  40318  cvrcon3b  40477  cvrat4  40643  3dim3  40669  ps-2  40678  llni  40708  llnle  40718  lplni  40732  lplnle  40740  lplnexllnN  40764  lvoli  40775  lnatexN  40979  elpaddn0  41000  pclfinN  41100  lhprelat3N  41240  4atexlemex2  41271  4atex  41276  4atex2-0aOLDN  41278  4atex2-0cOLDN  41280  lautcvr  41292  cdleme0ex1N  41423  cdleme50rnlem  41744  cdleme50ex  41759  cdlemg1cex  41788  cdlemkid5  42135  cdlemk  42174  tendoex  42175  cdleml5N  42180  cdlemm10N  42318  dih1dimatlem0  42528  dihjat1lem  42628  dvh3dim2  42648  dvh3dim3N  42649  dochkr1  42678  dochkr1OLDN  42679  lcfrvalsnN  42741  lcfrlem27  42769  lcfrlem37  42779  lcfr  42785  mapd1o  42848  mapdpglem23  42894  hdmap11lem2  43042  primrootsunit1  43290  zdivgd  43531  resubeu  43571  fidomncyc  43742  nacsfix  43866  mzpcompact2lem  43905  eldioph  43912  diophrw  43913  diophin  43926  rexrabdioph  43944  rexzrexnn0  43954  eldioph4b  43961  rencldnfilem  43970  irrapxlem5  43976  irrapxlem6  43977  pell1234qrdich  44011  pell14qrdich  44019  infmrgelbi  44028  pellqrex  44029  pellfundre  44031  pellfundlb  44034  rmxynorm  44068  congrep  44123  acongrep  44130  jm2.27  44158  islssfgi  44217  hbtlem2  44269  hbtlem4  44271  hbtlem5  44273  dgraaub  44293  mpaaeu  44295  aaitgo  44307  unielss  44363  onexgt  44385  onexomgt  44386  onexlimgt  44388  onexoegt  44389  oaordnr  44441  omnord1  44450  oenord1  44461  oaomoencom  44462  oenass  44464  tfsconcatfv2  44485  tfsconcatrn  44487  tfsconcatb0  44489  ofoafo  44501  naddcnffo  44509  oaun3lem1  44519  naddwordnexlem4  44546  sucomisnotcard  44688  clsk1independent  45189  0elaxnul  46115  pwclaxpow  46116  prclaxpr  46117  uniclaxun  46118  omssaxinf2  46120  wfac8prim  46134  restuni3  46275  iinssd  46288  founiiun  46336  wessf1ornlem  46342  founiiun0  46347  unirnmap  46363  dstregt0  46440  uzfissfz  46480  rpgtrecnn  46533  rexabslelem  46570  infrnmptle  46575  infxrunb3rnmpt  46580  infxrpnf  46598  supminfxr  46616  rexanuz2nf  46644  iooiinicc  46696  iooiinioc  46710  uzubioo  46719  climsuse  46762  islptre  46773  limsuppnfdlem  46853  climinf3  46868  limsupmnfuzlem  46878  limsupre3lem  46884  limsupre3uzlem  46887  0cnv  46894  liminfreuzlem  46954  cnrefiisplem  46981  icccncfext  47039  cncficcgt0  47040  dvbdfbdioo  47082  ioodvbdlimc1lem1  47083  ioodvbdlimc1lem2  47084  ioodvbdlimc2lem  47086  stoweidlem9  47161  stoweidlem14  47166  stoweidlem18  47170  stoweidlem21  47173  stoweidlem29  47181  stoweidlem34  47186  stoweidlem35  47187  stoweidlem39  47191  stoweidlem41  47193  stoweidlem45  47197  stoweidlem52  47204  stoweidlem55  47207  stoweidlem57  47209  stoweidlem60  47212  stirlinglem5  47230  stirlinglem13  47238  stirlinglem14  47239  fourierdlem16  47275  fourierdlem20  47279  fourierdlem21  47280  fourierdlem22  47281  fourierdlem25  47284  fourierdlem31  47290  fourierdlem39  47298  fourierdlem41  47300  fourierdlem42  47301  fourierdlem47  47305  fourierdlem48  47306  fourierdlem51  47309  fourierdlem63  47321  fourierdlem64  47322  fourierdlem65  47323  fourierdlem77  47335  fourierdlem81  47339  fourierdlem83  47341  fourierdlem103  47361  fourierdlem104  47362  elaa2lem  47385  etransclem47  47433  qndenserrnbl  47447  ioorrnopnlem  47456  ioorrnopnxrlem  47458  intsaluni  47481  salgencntex  47495  subsaliuncllem  47509  sge0resplit  47558  sge0seq  47598  sge0reuz  47599  nnfoctbdjlem  47607  meaiininclem  47638  hoicvrrex  47708  ovnlecvr  47710  ovnlerp  47714  hoidmv1lelem2  47744  hoidmvlelem2  47748  hoidmvlelem3  47749  ovnhoilem1  47753  ovnlecvr2  47762  hoiqssbl  47777  ovolval4lem2  47802  ovolval5lem2  47805  ovnovollem1  47808  ovnovollem2  47809  iinhoiicclem  47825  smfinflem  47969  smflimsuplem7  47978  sprsymrelfolem2  48717  perfectALTV  48963  9gbo  49014  11gbo  49015  nnsum3primes4  49028  nnsum3primesprm  49030  ssnn0ssfz  49603  lincsumcl  49685  lincscmcl  49686  zlmodzxzldep  49758  ldepsnlinc  49762  line2ylem  50005  sepfsepc  50184  lubsscl  50216  glbsscl  50217  nelsubc3lem  50326  cnelsubcw  50883  fuconuniqex  50928  fuconuniqex2  50929  aacllem  51156