Theorem rspcev 3577

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088

This theorem is used by:  rspcedvdw  3580  rspceaimv  3583  rspc2ev  3589  rspc3ev  3593  rspceeqv  3599  reu6i  3686  rspesbca  3828  eliuni  4957  iuneqconst  4963  brralrspcev  5165  wefrc  5645  wereu2  5648  xpdifid  6159  xpdifcnvepel  6160  frpomin  6343  onfr  6402  onelssex  6412  ordunidif  6413  eliman0  6922  dffv2  6980  elrnrexdm  7089  eldmrexrn  7091  elabrex  7246  elabrexg  7247  f1elima  7267  fliftfun  7320  fliftval  7324  f1oiso2  7360  sorpssuni  7748  sorpssint  7749  onssmin  7806  onminex  7816  fimaproj  8152  frxp3  8168  poseq  8175  tfrlem12  8397  seqomlem2  8461  oawordeulem  8562  oaass  8569  odi  8587  omass  8588  omeulem1  8590  oen0  8595  oelim2  8604  oeeulem  8610  nnawordex  8646  nnaordex2  8648  eldifsucnn  8673  cofon1  8681  cofon2  8682  naddcllem  8685  naddunif  8703  boxcutc  8969  0fi  9070  snfi  9071  rexdif1en  9176  findcard  9179  nnfi  9183  pssnn  9184  unfi  9186  onfin  9230  dif1ennnALT  9268  frfi  9276  fisupg  9279  nnsdomg  9291  pwfir  9308  prfi  9315  fissuni  9346  fipreima  9347  finsschain  9348  indexfi  9349  marypha1lem  9425  eqsup  9448  supmax  9460  fisup2g  9461  fisupcl  9462  supisoex  9467  infmin  9488  fiinfg  9493  fiinf2g  9494  wofib  9539  wemaplem2  9541  card2inf  9549  brwdom2  9567  cnfcom3clem  9706  ssttrcl  9716  ttrcltr  9717  trcl  9729  frmin  9753  r1ordg  9785  r1pwss  9791  tz9.12lem3  9796  tz9.12  9797  r1elwf  9804  tcrank  9901  elhf2  9910  0hf  9917  scottex  9933  scottexOLD  9934  scott0b  9937  scott0OLD  9938  isnumi  10027  onsdom  10077  ondomen  10116  infpwfien  10141  cardaleph  10168  infenaleph  10170  alephfplem4  10186  alephfp2  10188  dfac2b  10209  ackbij1lem18  10314  ackbij1  10315  cflem  10323  cflecard  10330  cfsuc  10335  cfflb  10337  cofsmo  10347  coftr  10351  fin23lem7  10394  fin23lem11  10395  enfin2i  10399  fin23lem26  10403  isf32lem5  10435  isf34lem4  10455  isfin1-3  10464  fin1a2lem7  10484  axdc3lem4  10531  ttukeylem7  10593  iunfo  10623  ficard  10649  pwcfsdom  10668  fpwwe2lem11  10726  wunex  10824  eltsk2g  10836  grur1  10905  axgroth6  10913  inaprc  10921  nqereu  11014  archnq  11065  genpnmax  11092  ltexpri  11128  prlem936  11132  recexpr  11136  supexpr  11139  negexsr  11187  recexsrlem  11188  recexsr  11192  supsrlem  11196  axrnegex  11247  axrrecex  11248  axpre-sup  11254  1re  11308  dedekind  11473  dedekindle  11474  cnegex  11491  cnegex2  11492  recex  11948  receu  11961  fiminre2  12265  cju  12316  nn2ge  12365  nominpos  12583  zdiv  12769  btwnz  12802  uzwo  13038  ublbneg  13060  lbzbi  13063  zsupss  13064  uzsupss  13067  rpnnen1lem1  13106  rpnnen1lem3  13107  rpnnen1lem4  13108  rpnnen1lem5  13109  z2ge  13328  qbtwnre  13329  qbtwnxr  13330  xralrple  13335  xrsupsslem  13437  xrinfmsslem  13438  supxrpnf  13448  icc0  13524  uzsup  14003  expnbnd  14376  expmulnbnd  14379  hashkf  14476  hashdom  14523  iswrdi  14662  rtrclreclem1  15210  rtrclreclem2  15212  rtrclreclem3  15213  01sqrex  15416  resqrex  15417  sqrtneg  15434  abs1m  15503  rexanuz  15513  rexuz3  15516  rexuzre  15520  sqreu  15528  o1lo1  15704  climconst  15710  rlimclim1  15712  climshftlem  15741  rlimo1  15784  lo1add  15794  lo1mul  15795  lo1le  15819  isercoll  15835  serf0  15848  zsum  15884  fsum  15886  fsumcvg3  15895  mertenslem1  16053  ntrivcvgn0  16067  ntrivcvgmullem  16070  zprod  16104  fprod  16108  fprodntriv  16109  dvdsval2  16425  dvds0lem  16436  dvds1lem  16437  dvds2lem  16438  odd2np1lem  16510  odd2np1  16511  opeo  16535  omeo  16536  divalglem9  16571  gcdcllem3  16671  lcmcllem  16771  qredeu  16833  exprmfct  16880  isprm5  16883  odzcllem  16970  reumodprminv  16982  modprm0  16983  nnnn0modprm0  16984  pythagtriplem19  17011  pcprmpw2  17060  pockthi  17085  infpnlem2  17089  vdwlem2  17160  vdwlem10  17168  vdwlem13  17171  ramub1lem1  17204  cshwrepswhash1  17280  imasleval  17713  mreexexlem3d  17820  mreexexlem4d  17821  iscatd  17847  cat1  18272  poslubd  18585  fpwipodrs  18714  ismgmid2  18849  mgmidsssn0  18853  mgmidpfod  18857  gsumval2a  18874  ismndd  18946  isgrpd2  19167  isgrpd  19169  imasgrp2  19265  mhmmnd  19274  ghmgrp  19276  gaorber  19522  orbsta  19527  cayleyth  19629  pmtrdifel  19694  pmtrdifwrdel  19699  pmtrdifwrdel2  19700  psgnunilem2  19709  psgnunilem3  19710  psgnvalii  19723  pgpfi1  19809  sylow1lem3  19814  sylow1lem5  19816  pgpfi  19819  sylow2alem2  19832  efgredeu  19966  lt6abl  20109  pgpfac1lem3a  20292  pgpfac1lem3  20293  pgpfac1lem5  20295  pgpfaclem1  20297  pgpfaclem3  20299  ablfaclem2  20302  dvdsrmul  20594  dvdsr01  20601  irredrmul  20657  rhmdvdsr  20758  rgspnval  20864  rgspncl  20865  lspf  21249  lspval  21250  lssats2  21275  lspfixed  21406  lspsolvlem  21420  zringlpir  21773  pzriprnglem13  21799  zncyg  21854  cygth  21877  frlmup4  22107  aspval  22180  evlseu  22392  matunitlindflem2  22995  fiinbas  23270  topbas  23290  pptbas  23326  clsval  23355  elcls  23391  neiint  23422  neips  23431  opnneissb  23432  opnssneib  23433  innei  23443  neiptopnei  23450  restbas  23476  neitr  23498  pnfnei  23538  mnfnei  23539  lmconst  23579  iscnp4  23581  cncnpi  23596  cnconst2  23601  cnprest  23607  cnpdis  23611  nrmsep  23675  regsep2  23694  cmpcovf  23709  cmpsub  23718  cmpcld  23720  hauscmplem  23724  conncompid  23749  2ndci  23766  2ndcsb  23767  2ndc1stc  23769  1stcrest  23771  2ndcctbss  23774  2ndcdisj  23775  2ndcomap  23777  2ndcsep  23778  dis2ndc  23779  restlly  23802  islly2  23803  hausllycmp  23813  cldllycmp  23814  lly1stc  23815  dislly  23816  ssref  23831  refref  23832  finlocfin  23839  dissnlocfin  23848  locfindis  23849  llycmpkgen2  23869  cmpkgen  23870  1stckgenlem  23872  elptr  23892  ptbasfi  23900  neitx  23926  ptpjopn  23931  txcnp  23939  ptcnplem  23940  txlly  23955  txnlly  23956  txtube  23959  txcmplem1  23960  tx1stc  23969  txkgen  23971  xkococnlem  23978  txconn  24008  tgqtop  24031  kqreglem1  24060  kqreglem2  24061  kqnrmlem1  24062  kqnrmlem2  24063  reghmph  24112  nrmhmph  24113  fbssfi  24156  opnfbas  24161  isfil2  24175  fsubbas  24186  ssfg  24191  fgss2  24193  fbasrn  24203  filuni  24204  fgtr  24209  ssufl  24237  uffix  24240  elfm2  24267  elfm3  24269  imaelfm  24270  rnelfmlem  24271  rnelfm  24272  fmfnfmlem4  24276  fmfnfm  24277  fmco  24280  ufldom  24281  hausflim  24300  flimcls  24304  hauspwpwf1  24306  flffbas  24314  txflf  24325  fclscf  24344  fclsfnflim  24346  alexsubALTlem4  24369  alexsubALT  24370  tmdgsum2  24415  symgtgp  24425  subgntr  24426  opnsubg  24427  ghmcnp  24434  qustgpopn  24439  tsmsfbas  24447  tsmsxplem1  24472  ustexsym  24535  trust  24548  utoptop  24553  restutop  24556  restutopopn  24557  ustuqtop4  24563  utopsnneiplem  24566  iducn  24601  fmucnd  24610  cfilufg  24611  trcfilu  24612  neipcfilu  24614  imasdsf1olem  24692  blssps  24743  blss  24744  blssexps  24745  blssex  24746  ssblex  24747  blin2  24748  neibl  24820  blcld  24824  metss2  24831  stdbdmopn  24837  met1stc  24840  met2ndci  24841  metrest  24843  prdsxmslem2  24848  metcnp3  24859  metustexhalf  24875  metustfbas  24876  cfilucfil  24878  restmetu  24889  dscopn  24892  ngptgp  24955  nlmvscnlem1  25005  tgioo  25115  tgqioo  25119  xrsmopn  25132  zcld  25133  recld2  25134  zdis  25136  icccmplem1  25142  icccmplem2  25143  xmetdcn2  25157  addcnlem  25184  xrhmeo  25267  cnheibor  25276  cnllycmp  25277  lebnumlem3  25284  lebnum  25285  xlebnum  25286  lebnumii  25287  elpi1i  25367  ipcnlem1  25566  lmnn  25584  iscfil3  25594  cfilres  25617  flimcfil  25635  bcthlem4  25648  bcthlem5  25649  minveclem4c  25746  minveclem2  25747  minveclem3b  25749  minveclem3  25750  minveclem4  25753  minveclem6  25755  ivthlem2  25773  ivth  25775  ivthle  25777  ivthle2  25778  elovolmr  25797  ovolunlem1  25818  ovoliunlem2  25824  ovolicc1  25837  iundisj  25869  iunmbl2  25878  dyadmbllem  25920  volivth  25928  mbflimsup  25987  i1faddlem  26014  i1fmullem  26015  itg2lr  26051  itg2monolem1  26071  limcnlp  26198  ellimc3  26199  limcflf  26201  limciun  26214  rollelem  26309  c1lip1  26317  lhop1lem  26333  ply1divex  26455  ig1peu  26493  elply2  26514  coeeq  26546  plydivlem3  26616  plydivlem4  26617  elqaalem3  26644  qaa  26647  iaaOLD  26652  aareccl  26653  aannenlem2  26656  aalioulem2  26660  aalioulem3  26661  aalioulem5  26663  aalioulem6  26664  aaliou  26665  aaliou2  26667  aaliou3lem8  26672  ulmshftlem  26716  reeff1o  26774  pilem2  26779  pilem3  26780  efif1olem2  26871  efopn  26986  cxpcn3lem  27075  cxpeq  27085  dcubic2  27172  quart  27189  xrlimcnp  27296  ftalem5  27404  ftalem7  27406  sgmnncl  27474  dvdsppwf1o  27513  musum  27518  perfect  27558  dchrptlem1  27591  dchrptlem2  27592  dchrpt  27594  bpos1lem  27609  lgsqrlem4  27676  lgsdchrval  27681  2sqblem  27758  dchrisumlem3  27818  chpdifbndlem2  27881  pntrsumbnd2  27894  pntpbnd1  27913  pntpbnd2  27914  pntpbnd  27915  pntibndlem2  27918  pntibndlem3  27919  pntleme  27935  pntlem3  27936  elno2  28011  ltsval2  28013  noreson  28017  ltsres  28019  noseponlem  28021  nolesgn2o  28028  nogesgn1o  28030  nodense  28049  nosupfv  28063  nosupres  28064  nosupbnd1lem3  28067  nosupbnd1lem5  28069  nosupbnd2lem1  28072  noinffv  28078  noinfres  28079  noinfbnd1lem3  28082  noinfbnd1lem5  28084  noinfbnd2lem1  28087  noetasuplem4  28093  noetainflem4  28097  noetalem2  28099  cuteq0  28201  cuteq1  28203  oldlim  28273  bdayiun  28301  cofcutrtime  28313  cofss  28316  coiniss  28317  cutlt  28318  cutmax  28320  cutmin  28321  negsex  28429  negsfo  28439  norecdiv  28576  divs1  28590  precsexlem11  28603  precsex  28604  recsex  28605  elons2d  28645  oncutlt  28650  n0on  28722  bdayn0sf1o  28756  dfnns2  28758  zsoring  28795  pw2recs  28824  halfcut  28844  0reno  28882  1reno  28883  readdscl  28885  axtgcont  28931  tgcgrxfr  28981  legid  29050  btwnleg  29051  leg0  29055  tghilberti1  29105  colline  29118  mirreu3  29126  isperp2  29190  colperpex  29209  lnopp2hpgb  29241  hpgerlem  29243  brbtwn  29477  brcgr  29478  brbtwn2  29483  axpasch  29519  axlowdimlem14  29533  axlowdim2  29538  axcontlem2  29543  axcontlem4  29545  axcontlem8  29549  axcontlem10  29551  axcontlem12  29553  fusgrn0degnn0  30080  loop1cycl  30744  umgr2cycllem  30746  umgr2cycl  30747  friendshipgt3  30999  lpni  31082  isgrpoi  31100  vacn  31296  smcnlem  31299  nmosetn0  31367  nmoolb  31373  nmobndi  31377  nmoo0  31393  nmlno0lem  31395  isblo3i  31403  blo3i  31404  blocnilem  31406  ubthlem1  31472  minvecolem2  31477  minvecolem3  31478  minvecolem4c  31481  minvecolem4  31482  minvecolem5  31483  minvecolem6  31484  norm1exi  31852  occl  31906  spanval  31935  spancl  31938  shsval2i  31989  ococin  32010  pjoml6i  32191  nmopsetn0  32467  nmfnsetn0  32480  nmoplb  32509  nmfnlb  32526  nmop0  32588  nmfn0  32589  nmlnop0iALT  32597  nmopun  32616  nmcexi  32628  lnconi  32635  lnopcnbd  32638  lnfncnbd  32659  riesz3i  32664  riesz1  32667  cnlnadjlem2  32670  cnlnadjlem8  32676  cnlnadjlem9  32677  adjbd1o  32687  branmfn  32707  opsqrlem1  32742  pjnmopi  32750  strlem1  32852  stri  32859  hstri  32867  cvcon3  32886  cvnbtwn  32888  superpos  32956  shatomici  32960  atcvat4i  32999  mdsymlem2  33006  cdj1i  33035  cdj3i  33043  rexunirn  33088  foresf1o  33100  iundisjf  33183  aciunf1lem  33256  fnpreimac  33264  fgreu  33265  fcnvgreu  33266  xrge0infss  33352  ssnnssfz  33379  iundisjfi  33388  indf1ofs  33433  xreceu  33488  rexdiv  33492  isarchi3  33748  archirngz  33750  archiabllem2a  33755  0nellinds  33926  qtophaus  34468  reff  34471  locfinreflem  34472  cmpcref  34482  dispcmp  34491  tpr2rico  34544  pnfneige0  34583  qqhucn  34624  rrhre  34653  esumcst  34695  esumpcvgval  34710  dmsigagen  34777  rossros  34813  dya2icoseg  34909  dya2iocnrect  34913  dya2iocuni  34915  eulerpartlemgvv  35008  dstfrvunirn  35107  ballotlem4  35131  ballotlemic  35139  ballotlemrc  35163  signsw0g  35185  signswmnd  35186  prodfzo03  35232  tgoldbachgt  35292  acwer1prclem  35759  onvf1odlem4  35885  subfacp1lem3  35947  erdsze2lem2  35969  cnpconn  35995  txpconn  35997  ptpconn  35998  indispconn  35999  connpconn  36000  cvxpconn  36007  cnllysconn  36010  cvmsss2  36039  cvmcov2  36040  cvmopnlem  36043  cvmliftlem14  36062  cvmliftlem15  36063  cvmlift2lem11  36078  cvmlift2lem12  36079  cvmlift2lem13  36080  cvmlift3lem2  36085  cvmlift3lem6  36089  cvmlift3lem9  36092  mthmi  36342  r1peuqusdeg1  36408  br8  36521  br6  36522  br4  36523  dfon2lem9  36553  wzel  36586  wsuclem  36587  wsuclb  36590  imagesset  36717  fvtransport  36797  brcolinear  36824  brsegle  36873  seglerflx  36877  seglemin  36878  btwnsegle  36882  fvray  36906  fvline  36909  hilbert1.1  36919  nn0prpwlem  37110  nn0prpw  37111  fness  37137  fneref  37138  fnessref  37145  refssfne  37146  neibastop2lem  37148  fnemeet1  37154  tailfb  37165  filnetlem4  37169  limsucncmpi  37233  ttctr  37281  dfttc2g  37294  taupilemrplb  38241  qdiff  38248  relowlssretop  38286  rdgellim  38299  ptrecube  38538  poimirlem4  38542  poimirlem17  38555  poimirlem20  38558  poimirlem23  38561  poimirlem24  38562  poimirlem26  38564  poimirlem27  38565  poimirlem29  38567  poimirlem32  38570  heicant  38573  mblfinlem1  38575  mblfinlem2  38576  mblfinlem3  38577  mblfinlem4  38578  ismblfin  38579  volsupnfl  38583  itg2addnclem  38589  itg2addnclem3  38591  itg2addnc  38592  ftc1anclem5  38615  unirep  38648  cover2  38649  indexa  38667  frinfm  38669  sdclem1  38677  fdc  38679  incsequz  38682  caushft  38695  istotbnd3  38705  0totbnd  38707  sstotbnd2  38708  sstotbnd  38709  sstotbnd3  38710  isbnd3  38718  ssbnd  38722  equivbnd  38724  prdsbnd  38727  prdstotbnd  38728  cntotbnd  38730  heibor1lem  38743  heiborlem1  38745  heiborlem3  38747  heiborlem6  38750  heiborlem8  38752  bfplem2  38757  rrncmslem  38766  iccbnd  38774  opidonOLD  38786  exidres  38812  isrngod  38832  isgrpda  38889  isdrngo2  38892  igenval  38995  igenidl  38997  prtlem10  39922  lshpnel2N  40042  lsmsat  40065  lssatomic  40068  lcvnbtwn  40082  lfl1  40127  eqlkr  40156  lshpkrlem1  40167  lshpkrex  40175  cvrcon3b  40334  cvrat4  40500  3dim3  40526  ps-2  40535  llni  40565  llnle  40575  lplni  40589  lplnle  40597  lplnexllnN  40621  lvoli  40632  lnatexN  40836  elpaddn0  40857  pclfinN  40957  lhprelat3N  41097  4atexlemex2  41128  4atex  41133  4atex2-0aOLDN  41135  4atex2-0cOLDN  41137  lautcvr  41149  cdleme0ex1N  41280  cdleme50rnlem  41601  cdleme50ex  41616  cdlemg1cex  41645  cdlemkid5  41992  cdlemk  42031  tendoex  42032  cdleml5N  42037  cdlemm10N  42175  dih1dimatlem0  42385  dihjat1lem  42485  dvh3dim2  42505  dvh3dim3N  42506  dochkr1  42535  dochkr1OLDN  42536  lcfrvalsnN  42598  lcfrlem27  42626  lcfrlem37  42636  lcfr  42642  mapd1o  42705  mapdpglem23  42751  hdmap11lem2  42899  primrootsunit1  43147  zdivgd  43388  resubeu  43428  fidomncyc  43599  nacsfix  43722  mzpcompact2lem  43761  eldioph  43768  diophrw  43769  diophin  43782  rexrabdioph  43800  rexzrexnn0  43810  eldioph4b  43817  rencldnfilem  43826  irrapxlem5  43832  irrapxlem6  43833  pell1234qrdich  43867  pell14qrdich  43875  infmrgelbi  43884  pellqrex  43885  pellfundre  43887  pellfundlb  43890  rmxynorm  43924  congrep  43979  acongrep  43986  jm2.27  44014  islssfgi  44073  hbtlem2  44125  hbtlem4  44127  hbtlem5  44129  dgraaub  44149  mpaaeu  44151  aaitgo  44163  unielss  44219  onexgt  44241  onexomgt  44242  onexlimgt  44244  onexoegt  44245  oaordnr  44297  omnord1  44306  oenord1  44317  oaomoencom  44318  oenass  44320  tfsconcatfv2  44341  tfsconcatrn  44343  tfsconcatb0  44345  ofoafo  44357  naddcnffo  44365  oaun3lem1  44375  naddwordnexlem4  44402  sucomisnotcard  44544  clsk1independent  45045  0elaxnul  45972  pwclaxpow  45973  prclaxpr  45974  uniclaxun  45975  omssaxinf2  45977  wfac8prim  45991  restuni3  46132  iinssd  46145  founiiun  46193  wessf1ornlem  46199  founiiun0  46204  unirnmap  46220  dstregt0  46297  uzfissfz  46337  rpgtrecnn  46390  rexabslelem  46427  infrnmptle  46432  infxrunb3rnmpt  46437  infxrpnf  46455  supminfxr  46473  rexanuz2nf  46501  iooiinicc  46553  iooiinioc  46567  uzubioo  46576  climsuse  46619  islptre  46630  limsuppnfdlem  46710  climinf3  46725  limsupmnfuzlem  46735  limsupre3lem  46741  limsupre3uzlem  46744  0cnv  46751  liminfreuzlem  46811  cnrefiisplem  46838  icccncfext  46896  cncficcgt0  46897  dvbdfbdioo  46939  ioodvbdlimc1lem1  46940  ioodvbdlimc1lem2  46941  ioodvbdlimc2lem  46943  stoweidlem9  47018  stoweidlem14  47023  stoweidlem18  47027  stoweidlem21  47030  stoweidlem29  47038  stoweidlem34  47043  stoweidlem35  47044  stoweidlem39  47048  stoweidlem41  47050  stoweidlem45  47054  stoweidlem52  47061  stoweidlem55  47064  stoweidlem57  47066  stoweidlem60  47069  stirlinglem5  47087  stirlinglem13  47095  stirlinglem14  47096  fourierdlem16  47132  fourierdlem20  47136  fourierdlem21  47137  fourierdlem22  47138  fourierdlem25  47141  fourierdlem31  47147  fourierdlem39  47155  fourierdlem41  47157  fourierdlem42  47158  fourierdlem47  47162  fourierdlem48  47163  fourierdlem51  47166  fourierdlem63  47178  fourierdlem64  47179  fourierdlem65  47180  fourierdlem77  47192  fourierdlem81  47196  fourierdlem83  47198  fourierdlem103  47218  fourierdlem104  47219  elaa2lem  47242  etransclem47  47290  qndenserrnbl  47304  ioorrnopnlem  47313  ioorrnopnxrlem  47315  intsaluni  47338  salgencntex  47352  subsaliuncllem  47366  sge0resplit  47415  sge0seq  47455  sge0reuz  47456  nnfoctbdjlem  47464  meaiininclem  47495  hoicvrrex  47565  ovnlecvr  47567  ovnlerp  47571  hoidmv1lelem2  47601  hoidmvlelem2  47605  hoidmvlelem3  47606  ovnhoilem1  47610  ovnlecvr2  47619  hoiqssbl  47634  ovolval4lem2  47659  ovolval5lem2  47662  ovnovollem1  47665  ovnovollem2  47666  iinhoiicclem  47682  smfinflem  47826  smflimsuplem7  47835  sprsymrelfolem2  48574  perfectALTV  48820  9gbo  48871  11gbo  48872  nnsum3primes4  48885  nnsum3primesprm  48887  ssnn0ssfz  49460  lincsumcl  49542  lincscmcl  49543  zlmodzxzldep  49615  ldepsnlinc  49619  line2ylem  49862  line2xlem  49864  sepfsepc  50035  lubsscl  50067  glbsscl  50068  nelsubc3lem  50177  cnelsubclem  50710  aacllem  50938