Theorem rspcev 3565

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063

This theorem is referenced by:  rspcedvdw  3568  rspceb2dv  3569  rspceaimv  3571  rspc2ev  3578  rspc3ev  3582  rspceeqv  3588  reu6i  3675  rspesbca  3820  eliuni  4940  iuneqconst  4946  brralrspcev  5146  wefrc  5616  wereu2  5619  xpdifid  6124  frpomin  6296  onfr  6354  onelssex  6364  ordunidif  6365  eliman0  6869  dffv2  6927  elrnrexdm  7033  eldmrexrn  7035  elabrex  7188  elabrexg  7189  f1elima  7209  fliftfun  7258  fliftval  7262  f1oiso2  7298  sorpssuni  7677  sorpssint  7678  onssmin  7737  onminex  7747  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  9615  ssttrcl  9625  ttrcltr  9626  trcl  9638  frmin  9662  r1ordg  9691  r1pwss  9697  tz9.12lem3  9702  tz9.12  9703  r1elwf  9709  tcrank  9797  scottex  9798  scott0  9799  isnumi  9859  onsdom  9909  ondomen  9948  infpwfien  9973  cardaleph  10000  infenaleph  10002  alephfplem4  10018  alephfp2  10020  dfac2b  10042  ackbij1lem18  10147  ackbij1  10148  cflem  10156  cflemOLD  10157  cflecard  10164  cfsuc  10168  cfflb  10170  cofsmo  10180  coftr  10184  fin23lem7  10227  fin23lem11  10228  enfin2i  10232  fin23lem26  10236  isf32lem5  10268  isf34lem4  10288  isfin1-3  10297  fin1a2lem7  10317  axdc3lem4  10364  ttukeylem7  10426  iunfo  10450  ficard  10476  pwcfsdom  10495  fpwwe2lem11  10553  wunex  10651  eltsk2g  10663  grur1  10732  axgroth6  10740  inaprc  10748  nqereu  10841  archnq  10892  genpnmax  10919  ltexpri  10955  prlem936  10959  recexpr  10963  supexpr  10966  negexsr  11014  recexsrlem  11015  recexsr  11019  supsrlem  11023  axrnegex  11074  axrrecex  11075  axpre-sup  11081  1re  11133  dedekind  11298  dedekindle  11299  cnegex  11316  cnegex2  11317  recex  11771  receu  11784  fiminre2  12093  cju  12144  nn2ge  12193  nominpos  12403  zdiv  12588  btwnz  12621  uzwo  12850  ublbneg  12872  lbzbi  12875  zsupss  12876  uzsupss  12879  rpnnen1lem1  12917  rpnnen1lem3  12918  rpnnen1lem4  12919  rpnnen1lem5  12920  z2ge  13139  qbtwnre  13140  qbtwnxr  13141  xralrple  13146  xrsupsslem  13248  xrinfmsslem  13249  supxrpnf  13259  icc0  13335  uzsup  13811  expnbnd  14183  expmulnbnd  14186  hashkf  14283  hashdom  14330  iswrdi  14468  rtrclreclem1  15008  rtrclreclem2  15010  rtrclreclem3  15011  01sqrex  15200  resqrex  15201  sqrtneg  15218  abs1m  15287  rexanuz  15297  rexuz3  15300  rexuzre  15304  sqreu  15312  o1lo1  15488  climconst  15494  rlimclim1  15496  climshftlem  15525  rlimo1  15568  lo1add  15578  lo1mul  15579  lo1le  15603  isercoll  15619  serf0  15632  zsum  15669  fsum  15671  fsumcvg3  15680  mertenslem1  15838  ntrivcvgn0  15852  ntrivcvgmullem  15855  zprod  15891  fprod  15895  fprodntriv  15896  dvdsval2  16213  dvds0lem  16224  dvds1lem  16225  dvds2lem  16226  odd2np1lem  16298  odd2np1  16299  opeo  16323  omeo  16324  divalglem9  16359  gcdcllem3  16459  lcmcllem  16554  qredeu  16616  exprmfct  16663  isprm5  16666  odzcllem  16752  reumodprminv  16764  modprm0  16765  nnnn0modprm0  16766  pythagtriplem19  16793  pcprmpw2  16842  pockthi  16867  infpnlem2  16871  vdwlem2  16942  vdwlem10  16950  vdwlem13  16953  ramub1lem1  16986  cshwrepswhash1  17062  imasleval  17494  mreexexlem3d  17601  mreexexlem4d  17602  iscatd  17628  cat1  18053  poslubd  18366  fpwipodrs  18495  ismgmid2  18625  mgmidsssn0  18629  gsumval2a  18642  ismndd  18713  isgrpd2  18921  isgrpd  18923  imasgrp2  19020  mhmmnd  19029  ghmgrp  19031  gaorber  19272  orbsta  19277  cayleyth  19379  pmtrdifel  19444  pmtrdifwrdel  19449  pmtrdifwrdel2  19450  psgnunilem2  19459  psgnunilem3  19460  psgnvalii  19473  pgpfi1  19559  sylow1lem3  19564  sylow1lem5  19566  pgpfi  19569  sylow2alem2  19582  efgredeu  19716  lt6abl  19859  pgpfac1lem3a  20042  pgpfac1lem3  20043  pgpfac1lem5  20045  pgpfaclem1  20047  pgpfaclem3  20049  ablfaclem2  20052  dvdsrmul  20333  dvdsr01  20340  irredrmul  20396  rhmdvdsr  20474  rgspnval  20578  rgspncl  20579  lspf  20958  lspval  20959  lssats2  20984  lspfixed  21116  lspsolvlem  21130  zringlpir  21455  pzriprnglem13  21481  zncyg  21536  cygth  21559  frlmup4  21789  aspval  21860  evlseu  22070  fiinbas  22926  topbas  22946  pptbas  22982  clsval  23011  elcls  23047  neiint  23078  neips  23087  opnneissb  23088  opnssneib  23089  innei  23099  neiptopnei  23106  restbas  23132  neitr  23154  pnfnei  23194  mnfnei  23195  lmconst  23235  iscnp4  23237  cncnpi  23252  cnconst2  23257  cnprest  23263  cnpdis  23267  nrmsep  23331  regsep2  23350  cmpcovf  23365  cmpsub  23374  cmpcld  23376  hauscmplem  23380  conncompid  23405  2ndci  23422  2ndcsb  23423  2ndc1stc  23425  1stcrest  23427  2ndcctbss  23429  2ndcdisj  23430  2ndcomap  23432  2ndcsep  23433  dis2ndc  23434  restlly  23457  islly2  23458  hausllycmp  23468  cldllycmp  23469  lly1stc  23470  dislly  23471  ssref  23486  refref  23487  finlocfin  23494  dissnlocfin  23503  locfindis  23504  llycmpkgen2  23524  cmpkgen  23525  1stckgenlem  23527  elptr  23547  ptbasfi  23555  neitx  23581  ptpjopn  23586  txcnp  23594  ptcnplem  23595  txlly  23610  txnlly  23611  txtube  23614  txcmplem1  23615  tx1stc  23624  txkgen  23626  xkococnlem  23633  txconn  23663  tgqtop  23686  kqreglem1  23715  kqreglem2  23716  kqnrmlem1  23717  kqnrmlem2  23718  reghmph  23767  nrmhmph  23768  fbssfi  23811  opnfbas  23816  isfil2  23830  fsubbas  23841  ssfg  23846  fgss2  23848  fbasrn  23858  filuni  23859  fgtr  23864  ssufl  23892  uffix  23895  elfm2  23922  elfm3  23924  imaelfm  23925  rnelfmlem  23926  rnelfm  23927  fmfnfmlem4  23931  fmfnfm  23932  fmco  23935  ufldom  23936  hausflim  23955  flimcls  23959  hauspwpwf1  23961  flffbas  23969  txflf  23980  fclscf  23999  fclsfnflim  24001  alexsubALTlem4  24024  alexsubALT  24025  tmdgsum2  24070  symgtgp  24080  subgntr  24081  opnsubg  24082  ghmcnp  24089  qustgpopn  24094  tsmsfbas  24102  tsmsxplem1  24127  ustexsym  24190  trust  24203  utoptop  24208  restutop  24211  restutopopn  24212  ustuqtop4  24218  utopsnneiplem  24221  iducn  24256  fmucnd  24265  cfilufg  24266  trcfilu  24267  neipcfilu  24269  imasdsf1olem  24347  blssps  24398  blss  24399  blssexps  24400  blssex  24401  ssblex  24402  blin2  24403  neibl  24475  blcld  24479  metss2  24486  stdbdmopn  24492  met1stc  24495  met2ndci  24496  metrest  24498  prdsxmslem2  24503  metcnp3  24514  metustexhalf  24530  metustfbas  24531  cfilucfil  24533  restmetu  24544  dscopn  24547  ngptgp  24610  nlmvscnlem1  24660  tgioo  24770  tgqioo  24774  xrsmopn  24787  zcld  24788  recld2  24789  zdis  24791  icccmplem1  24797  icccmplem2  24798  xmetdcn2  24812  addcnlem  24839  xrhmeo  24922  cnheibor  24931  cnllycmp  24932  lebnumlem3  24939  lebnum  24940  xlebnum  24941  lebnumii  24942  elpi1i  25022  ipcnlem1  25221  lmnn  25239  iscfil3  25249  cfilres  25272  flimcfil  25290  bcthlem4  25303  bcthlem5  25304  minveclem4c  25401  minveclem2  25402  minveclem3b  25404  minveclem3  25405  minveclem4  25408  minveclem6  25410  ivthlem2  25428  ivth  25430  ivthle  25432  ivthle2  25433  elovolmr  25452  ovolunlem1  25473  ovoliunlem2  25479  ovolicc1  25492  iundisj  25524  iunmbl2  25533  dyadmbllem  25575  volivth  25583  mbflimsup  25642  i1faddlem  25669  i1fmullem  25670  itg2lr  25706  itg2monolem1  25726  limcnlp  25854  ellimc3  25855  limcflf  25857  limciun  25870  rollelem  25965  c1lip1  25974  lhop1lem  25990  ply1divex  26114  ig1peu  26152  elply2  26173  coeeq  26204  plydivlem3  26274  plydivlem4  26275  elqaalem3  26300  qaa  26302  iaa  26304  aareccl  26305  aannenlem2  26308  aalioulem2  26312  aalioulem3  26313  aalioulem5  26315  aalioulem6  26316  aaliou  26317  aaliou2  26319  aaliou3lem8  26324  ulmshftlem  26369  reeff1o  26428  pilem2  26433  pilem3  26434  efif1olem2  26523  efopn  26638  cxpcn3lem  26728  cxpeq  26738  dcubic2  26825  quart  26842  xrlimcnp  26949  ftalem5  27058  ftalem7  27060  sgmnncl  27128  dvdsppwf1o  27167  musum  27172  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  29588  friendshipgt3  30488  lpni  30571  isgrpoi  30589  vacn  30785  smcnlem  30788  nmosetn0  30856  nmoolb  30862  nmobndi  30866  nmoo0  30882  nmlno0lem  30884  isblo3i  30892  blo3i  30893  blocnilem  30895  ubthlem1  30961  minvecolem2  30966  minvecolem3  30967  minvecolem4c  30970  minvecolem4  30971  minvecolem5  30972  minvecolem6  30973  norm1exi  31341  occl  31395  spanval  31424  spancl  31427  shsval2i  31478  ococin  31499  pjoml6i  31680  nmopsetn0  31956  nmfnsetn0  31969  nmoplb  31998  nmfnlb  32015  nmop0  32077  nmfn0  32078  nmlnop0iALT  32086  nmopun  32105  nmcexi  32117  lnconi  32124  lnopcnbd  32127  lnfncnbd  32148  riesz3i  32153  riesz1  32156  cnlnadjlem2  32159  cnlnadjlem8  32165  cnlnadjlem9  32166  adjbd1o  32176  branmfn  32196  opsqrlem1  32231  pjnmopi  32239  strlem1  32341  stri  32348  hstri  32356  cvcon3  32375  cvnbtwn  32377  superpos  32445  shatomici  32449  atcvat4i  32488  mdsymlem2  32495  cdj1i  32524  cdj3i  32532  rexunirn  32581  foresf1o  32594  iundisjf  32679  aciunf1lem  32755  fnpreimac  32763  fgreu  32764  fcnvgreu  32765  xrge0infss  32853  ssnnssfz  32880  iundisjfi  32889  indf1ofs  32946  xreceu  33001  rexdiv  33005  isarchi3  33268  archirngz  33270  archiabllem2a  33275  0nellinds  33450  qtophaus  34001  reff  34004  locfinreflem  34005  cmpcref  34015  dispcmp  34024  tpr2rico  34077  pnfneige0  34116  qqhucn  34157  rrhre  34186  esumcst  34228  esumpcvgval  34243  dmsigagen  34309  rossros  34345  dya2icoseg  34442  dya2iocnrect  34446  dya2iocuni  34448  eulerpartlemgvv  34541  dstfrvunirn  34640  ballotlem4  34664  ballotlemic  34672  ballotlem1c  34673  ballotlemrc  34696  signsw0g  34721  signswmnd  34722  prodfzo03  34768  tgoldbachgt  34828  onvf1odlem4  35309  loop1cycl  35340  umgr2cycllem  35343  umgr2cycl  35344  subfacp1lem3  35385  erdsze2lem2  35407  cnpconn  35433  txpconn  35435  ptpconn  35436  indispconn  35437  connpconn  35438  cvxpconn  35445  cnllysconn  35448  cvmsss2  35477  cvmcov2  35478  cvmopnlem  35481  cvmliftlem14  35500  cvmliftlem15  35501  cvmlift2lem11  35516  cvmlift2lem12  35517  cvmlift2lem13  35518  cvmlift3lem2  35523  cvmlift3lem6  35527  cvmlift3lem9  35530  mthmi  35780  r1peuqusdeg1  35846  br8  35959  br6  35960  br4  35961  dfon2lem9  35992  wzel  36025  wsuclem  36026  wsuclb  36029  imagesset  36156  fvtransport  36235  brcolinear  36262  brsegle  36311  seglerflx  36315  seglemin  36316  btwnsegle  36320  fvray  36344  fvline  36347  hilbert1.1  36357  elhf2  36378  0hf  36380  nn0prpwlem  36525  nn0prpw  36526  fness  36552  fneref  36553  fnessref  36560  refssfne  36561  neibastop2lem  36563  fnemeet1  36569  tailfb  36580  filnetlem4  36584  limsucncmpi  36648  ttctr  36696  dfttc2g  36709  taupilemrplb  37647  relowlssretop  37690  rdgellim  37703  matunitlindflem2  37949  ptrecube  37952  poimirlem4  37956  poimirlem17  37969  poimirlem20  37972  poimirlem23  37975  poimirlem24  37976  poimirlem26  37978  poimirlem27  37979  poimirlem29  37981  poimirlem32  37984  heicant  37987  mblfinlem1  37989  mblfinlem2  37990  mblfinlem3  37991  mblfinlem4  37992  ismblfin  37993  volsupnfl  37997  itg2addnclem  38003  itg2addnclem3  38005  itg2addnc  38006  ftc1anclem5  38029  unirep  38046  cover2  38047  indexa  38065  frinfm  38067  sdclem1  38075  fdc  38077  incsequz  38080  caushft  38093  istotbnd3  38103  0totbnd  38105  sstotbnd2  38106  sstotbnd  38107  sstotbnd3  38108  isbnd3  38116  ssbnd  38120  equivbnd  38122  prdsbnd  38125  prdstotbnd  38126  cntotbnd  38128  heibor1lem  38141  heiborlem1  38143  heiborlem3  38145  heiborlem6  38148  heiborlem8  38150  bfplem2  38155  rrncmslem  38164  iccbnd  38172  opidonOLD  38184  exidres  38210  isrngod  38230  isgrpda  38287  isdrngo2  38290  igenval  38393  igenidl  38395  prtlem10  39322  lshpnel2N  39442  lsmsat  39465  lssatomic  39468  lcvnbtwn  39482  lfl1  39527  eqlkr  39556  lshpkrlem1  39567  lshpkrex  39575  cvrcon3b  39734  cvrat4  39900  3dim3  39926  ps-2  39935  llni  39965  llnle  39975  lplni  39989  lplnle  39997  lplnexllnN  40021  lvoli  40032  lnatexN  40236  elpaddn0  40257  pclfinN  40357  lhprelat3N  40497  4atexlemex2  40528  4atex  40533  4atex2-0aOLDN  40535  4atex2-0cOLDN  40537  lautcvr  40549  cdleme0ex1N  40680  cdleme50rnlem  41001  cdleme50ex  41016  cdlemg1cex  41045  cdlemkid5  41392  cdlemk  41431  tendoex  41432  cdleml5N  41437  cdlemm10N  41575  dih1dimatlem0  41785  dihjat1lem  41885  dvh3dim2  41905  dvh3dim3N  41906  dochkr1  41935  dochkr1OLDN  41936  lcfrvalsnN  41998  lcfrlem27  42026  lcfrlem37  42036  lcfr  42042  mapd1o  42105  mapdpglem23  42151  hdmap11lem2  42299  primrootsunit1  42547  zdivgd  42780  resubeu  42820  fidomncyc  42991  nacsfix  43155  mzpcompact2lem  43194  eldioph  43201  diophrw  43202  diophin  43215  rexrabdioph  43237  rexzrexnn0  43247  eldioph4b  43254  rencldnfilem  43263  irrapxlem5  43269  irrapxlem6  43270  pell1234qrdich  43304  pell14qrdich  43312  infmrgelbi  43321  pellqrex  43322  pellfundre  43324  pellfundlb  43327  rmxynorm  43361  congrep  43416  acongrep  43423  jm2.27  43451  fnwe2lem2  43494  islssfgi  43515  hbtlem2  43567  hbtlem4  43569  hbtlem5  43571  dgraaub  43591  mpaaeu  43593  aaitgo  43605  unielss  43661  onexgt  43683  onexomgt  43684  onexlimgt  43686  onexoegt  43687  oaordnr  43739  omnord1  43748  oenord1  43759  oaomoencom  43760  oenass  43762  tfsconcatfv2  43783  tfsconcatrn  43785  tfsconcatb0  43787  ofoafo  43799  naddcnffo  43807  oaun3lem1  43817  naddwordnexlem4  43844  sucomisnotcard  43986  clsk1independent  44488  0elaxnul  45425  pwclaxpow  45426  prclaxpr  45427  uniclaxun  45428  omssaxinf2  45430  wfac8prim  45444  restuni3  45563  iinssd  45576  founiiun  45624  wessf1ornlem  45630  founiiun0  45635  unirnmap  45652  dstregt0  45730  uzfissfz  45771  rpgtrecnn  45824  rexabslelem  45861  infrnmptle  45866  infxrunb3rnmpt  45871  infxrpnf  45889  supminfxr  45907  rexanuz2nf  45935  iooiinicc  45987  iooiinioc  46001  uzubioo  46010  climsuse  46053  islptre  46064  limsuppnfdlem  46144  climinf3  46159  limsupmnfuzlem  46169  limsupre3lem  46175  limsupre3uzlem  46178  0cnv  46185  liminfreuzlem  46245  cnrefiisplem  46272  icccncfext  46330  cncficcgt0  46331  dvbdfbdioo  46373  ioodvbdlimc1lem1  46374  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  stoweidlem9  46452  stoweidlem14  46457  stoweidlem18  46461  stoweidlem21  46464  stoweidlem29  46472  stoweidlem34  46477  stoweidlem35  46478  stoweidlem39  46482  stoweidlem41  46484  stoweidlem45  46488  stoweidlem52  46495  stoweidlem55  46498  stoweidlem57  46500  stoweidlem60  46503  stirlinglem5  46521  stirlinglem13  46529  stirlinglem14  46530  fourierdlem16  46566  fourierdlem20  46570  fourierdlem21  46571  fourierdlem22  46572  fourierdlem25  46575  fourierdlem31  46581  fourierdlem39  46589  fourierdlem41  46591  fourierdlem42  46592  fourierdlem47  46596  fourierdlem48  46597  fourierdlem49  46598  fourierdlem51  46600  fourierdlem63  46612  fourierdlem64  46613  fourierdlem65  46614  fourierdlem77  46626  fourierdlem81  46630  fourierdlem83  46632  fourierdlem103  46652  fourierdlem104  46653  elaa2lem  46676  etransclem47  46724  qndenserrnbl  46738  ioorrnopnlem  46747  ioorrnopnxrlem  46749  intsaluni  46772  salgencntex  46786  subsaliuncllem  46800  sge0resplit  46849  sge0seq  46889  sge0reuz  46890  nnfoctbdjlem  46898  meaiininclem  46929  hoicvrrex  46999  ovnlecvr  47001  ovnlerp  47005  hoidmv1lelem2  47035  hoidmvlelem2  47039  hoidmvlelem3  47040  ovnhoilem1  47044  ovnlecvr2  47053  hoiqssbl  47068  ovolval4lem2  47093  ovolval5lem2  47096  ovnovollem1  47099  ovnovollem2  47100  iinhoiicclem  47116  smfinflem  47260  smflimsuplem7  47269  nthrucw  47329  sprsymrelfolem2  47950  perfectALTV  48196  9gbo  48247  11gbo  48248  nnsum3primes4  48261  nnsum3primesprm  48263  ssnn0ssfz  48822  lincsumcl  48904  lincscmcl  48905  zlmodzxzldep  48977  ldepsnlinc  48981  line2ylem  49224  line2xlem  49226  sepfsepc  49400  lubsscl  49432  glbsscl  49433  nelsubc3lem  49542  cnelsubclem  50075  aacllem  50273