Theorem rspcev 3622

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∃wrex 3070

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071

This theorem is referenced by:  rspcedvdw  3625  rspceb2dv  3626  rspceaimv  3628  rspc2ev  3635  rspc3ev  3639  rspceeqv  3645  reu6i  3734  rspesbca  3881  eliuni  4997  iuneqconst  5003  brralrspcev  5203  wefrc  5679  wereu2  5682  xpdifid  6188  frpomin  6361  onfr  6423  onelssex  6432  ordunidif  6433  eliman0  6946  dffv2  7004  elrnrexdm  7109  eldmrexrn  7111  elabrex  7262  elabrexg  7263  elunirn2OLD  7273  f1elima  7283  fliftfun  7332  fliftval  7336  f1oiso2  7372  sorpssuni  7752  sorpssint  7753  onssmin  7812  onminex  7822  fimaproj  8160  frxp3  8176  poseq  8183  tfrlem12  8429  seqomlem2  8491  oawordeulem  8592  oaass  8599  odi  8617  omass  8618  omeulem1  8620  oen0  8624  oelim2  8633  oeeulem  8639  nnawordex  8675  nnaordex2  8677  eldifsucnn  8702  cofon1  8710  cofon2  8711  naddcllem  8714  naddunif  8731  boxcutc  8981  0fi  9082  snfi  9083  snfiOLD  9084  rexdif1en  9198  rexdif1enOLD  9199  findcard  9203  nnfi  9207  pssnn  9208  unfi  9211  onfin  9267  dif1ennnALT  9311  frfi  9321  fisupg  9324  nnsdomg  9335  nnsdomgOLD  9336  pwfir  9355  prfi  9363  fissuni  9397  fipreima  9398  finsschain  9399  indexfi  9400  marypha1lem  9473  eqsup  9496  supmax  9507  fisup2g  9508  fisupcl  9509  supisoex  9514  infmin  9534  fiinfg  9539  fiinf2g  9540  wofib  9585  wemaplem2  9587  card2inf  9595  brwdom2  9613  cnfcom3clem  9745  ssttrcl  9755  ttrcltr  9756  trcl  9768  frmin  9789  r1ordg  9818  r1pwss  9824  tz9.12lem3  9829  tz9.12  9830  r1elwf  9836  tcrank  9924  scottex  9925  scott0  9926  isnumi  9986  onsdom  10036  ondomen  10077  infpwfien  10102  cardaleph  10129  infenaleph  10131  alephfplem4  10147  alephfp2  10149  dfac2b  10171  ackbij1lem18  10276  ackbij1  10277  cflem  10285  cflemOLD  10286  cflecard  10293  cfsuc  10297  cfflb  10299  cofsmo  10309  coftr  10313  fin23lem7  10356  fin23lem11  10357  enfin2i  10361  fin23lem26  10365  isf32lem5  10397  isf34lem4  10417  isfin1-3  10426  fin1a2lem7  10446  axdc3lem4  10493  ttukeylem7  10555  iunfo  10579  ficard  10605  pwcfsdom  10623  fpwwe2lem11  10681  wunex  10779  eltsk2g  10791  grur1  10860  axgroth6  10868  inaprc  10876  nqereu  10969  archnq  11020  genpnmax  11047  ltexpri  11083  prlem936  11087  recexpr  11091  supexpr  11094  negexsr  11142  recexsrlem  11143  recexsr  11147  supsrlem  11151  axrnegex  11202  axrrecex  11203  axpre-sup  11209  1re  11261  dedekind  11424  dedekindle  11425  cnegex  11442  cnegex2  11443  recex  11895  receu  11908  fiminre2  12216  cju  12262  nn2ge  12293  nominpos  12503  zdiv  12688  btwnz  12721  uzwo  12953  ublbneg  12975  lbzbi  12978  zsupss  12979  uzsupss  12982  rpnnen1lem1  13020  rpnnen1lem3  13021  rpnnen1lem4  13022  rpnnen1lem5  13023  z2ge  13240  qbtwnre  13241  qbtwnxr  13242  xralrple  13247  xrsupsslem  13349  xrinfmsslem  13350  supxrpnf  13360  icc0  13435  uzsup  13903  expnbnd  14271  expmulnbnd  14274  hashkf  14371  hashdom  14418  iswrdi  14556  rtrclreclem1  15096  rtrclreclem2  15098  rtrclreclem3  15099  01sqrex  15288  resqrex  15289  sqrtneg  15306  abs1m  15374  rexanuz  15384  rexuz3  15387  rexuzre  15391  sqreu  15399  o1lo1  15573  climconst  15579  rlimclim1  15581  climshftlem  15610  rlimo1  15653  lo1add  15663  lo1mul  15664  lo1le  15688  isercoll  15704  serf0  15717  zsum  15754  fsum  15756  fsumcvg3  15765  mertenslem1  15920  ntrivcvgn0  15934  ntrivcvgmullem  15937  zprod  15973  fprod  15977  fprodntriv  15978  dvdsval2  16293  dvds0lem  16304  dvds1lem  16305  dvds2lem  16306  odd2np1lem  16377  odd2np1  16378  opeo  16402  omeo  16403  divalglem9  16438  gcdcllem3  16538  lcmcllem  16633  qredeu  16695  exprmfct  16741  isprm5  16744  odzcllem  16830  reumodprminv  16842  modprm0  16843  nnnn0modprm0  16844  pythagtriplem19  16871  pcprmpw2  16920  pockthi  16945  infpnlem2  16949  vdwlem2  17020  vdwlem10  17028  vdwlem13  17031  ramub1lem1  17064  cshwrepswhash1  17140  imasleval  17586  mreexexlem3d  17689  mreexexlem4d  17690  iscatd  17716  cat1  18142  poslubd  18458  fpwipodrs  18585  ismgmid2  18681  mgmidsssn0  18685  gsumval2a  18698  ismndd  18769  isgrpd2  18974  isgrpd  18976  imasgrp2  19073  mhmmnd  19082  ghmgrp  19084  gaorber  19326  orbsta  19331  cayleyth  19433  pmtrdifel  19498  pmtrdifwrdel  19503  pmtrdifwrdel2  19504  psgnunilem2  19513  psgnunilem3  19514  psgnvalii  19527  pgpfi1  19613  sylow1lem3  19618  sylow1lem5  19620  pgpfi  19623  sylow2alem2  19636  efgredeu  19770  lt6abl  19913  pgpfac1lem3a  20096  pgpfac1lem3  20097  pgpfac1lem5  20099  pgpfaclem1  20101  pgpfaclem3  20103  ablfaclem2  20106  dvdsrmul  20364  dvdsr01  20371  irredrmul  20427  rhmdvdsr  20508  rgspnval  20612  rgspncl  20613  lspf  20972  lspval  20973  lssats2  20998  lspfixed  21130  lspsolvlem  21144  zringlpir  21478  pzriprnglem13  21504  zncyg  21567  cygth  21590  frlmup4  21821  aspval  21893  evlseu  22107  fiinbas  22959  topbas  22979  pptbas  23015  clsval  23045  elcls  23081  neiint  23112  neips  23121  opnneissb  23122  opnssneib  23123  innei  23133  neiptopnei  23140  restbas  23166  neitr  23188  pnfnei  23228  mnfnei  23229  lmconst  23269  iscnp4  23271  cncnpi  23286  cnconst2  23291  cnprest  23297  cnpdis  23301  nrmsep  23365  regsep2  23384  cmpcovf  23399  cmpsub  23408  cmpcld  23410  hauscmplem  23414  conncompid  23439  2ndci  23456  2ndcsb  23457  2ndc1stc  23459  1stcrest  23461  2ndcctbss  23463  2ndcdisj  23464  2ndcomap  23466  2ndcsep  23467  dis2ndc  23468  restlly  23491  islly2  23492  hausllycmp  23502  cldllycmp  23503  lly1stc  23504  dislly  23505  ssref  23520  refref  23521  finlocfin  23528  dissnlocfin  23537  locfindis  23538  llycmpkgen2  23558  cmpkgen  23559  1stckgenlem  23561  elptr  23581  ptbasfi  23589  neitx  23615  ptpjopn  23620  txcnp  23628  ptcnplem  23629  txlly  23644  txnlly  23645  txtube  23648  txcmplem1  23649  tx1stc  23658  txkgen  23660  xkococnlem  23667  txconn  23697  tgqtop  23720  kqreglem1  23749  kqreglem2  23750  kqnrmlem1  23751  kqnrmlem2  23752  reghmph  23801  nrmhmph  23802  fbssfi  23845  opnfbas  23850  isfil2  23864  fsubbas  23875  ssfg  23880  fgss2  23882  fbasrn  23892  filuni  23893  fgtr  23898  ssufl  23926  uffix  23929  elfm2  23956  elfm3  23958  imaelfm  23959  rnelfmlem  23960  rnelfm  23961  fmfnfmlem4  23965  fmfnfm  23966  fmco  23969  ufldom  23970  hausflim  23989  flimcls  23993  hauspwpwf1  23995  flffbas  24003  txflf  24014  fclscf  24033  fclsfnflim  24035  alexsubALTlem4  24058  alexsubALT  24059  tmdgsum2  24104  symgtgp  24114  subgntr  24115  opnsubg  24116  ghmcnp  24123  qustgpopn  24128  tsmsfbas  24136  tsmsxplem1  24161  ustexsym  24224  trust  24238  utoptop  24243  restutop  24246  restutopopn  24247  ustuqtop4  24253  utopsnneiplem  24256  iducn  24292  fmucnd  24301  cfilufg  24302  trcfilu  24303  neipcfilu  24305  imasdsf1olem  24383  blssps  24434  blss  24435  blssexps  24436  blssex  24437  ssblex  24438  blin2  24439  neibl  24514  blcld  24518  metss2  24525  stdbdmopn  24531  met1stc  24534  met2ndci  24535  metrest  24537  prdsxmslem2  24542  metcnp3  24553  metustexhalf  24569  metustfbas  24570  cfilucfil  24572  restmetu  24583  dscopn  24586  ngptgp  24649  nlmvscnlem1  24707  tgioo  24817  tgqioo  24821  xrsmopn  24834  zcld  24835  recld2  24836  zdis  24838  icccmplem1  24844  icccmplem2  24845  xmetdcn2  24859  addcnlem  24886  xrhmeo  24977  cnheibor  24987  cnllycmp  24988  lebnumlem3  24995  lebnum  24996  xlebnum  24997  lebnumii  24998  elpi1i  25079  ipcnlem1  25279  lmnn  25297  iscfil3  25307  cfilres  25330  flimcfil  25348  bcthlem4  25361  bcthlem5  25362  minveclem4c  25459  minveclem2  25460  minveclem3b  25462  minveclem3  25463  minveclem4  25466  minveclem6  25468  ivthlem2  25487  ivth  25489  ivthle  25491  ivthle2  25492  elovolmr  25511  ovolunlem1  25532  ovoliunlem2  25538  ovolicc1  25551  iundisj  25583  iunmbl2  25592  dyadmbllem  25634  volivth  25642  mbflimsup  25701  i1faddlem  25728  i1fmullem  25729  itg2lr  25765  itg2monolem1  25785  limcnlp  25913  ellimc3  25914  limcflf  25916  limciun  25929  rollelem  26027  c1lip1  26036  lhop1lem  26052  ply1divex  26176  ig1peu  26214  elply2  26235  coeeq  26266  plydivlem3  26337  plydivlem4  26338  elqaalem3  26363  qaa  26365  iaa  26367  aareccl  26368  aannenlem2  26371  aalioulem2  26375  aalioulem3  26376  aalioulem5  26378  aalioulem6  26379  aaliou  26380  aaliou2  26382  aaliou3lem8  26387  ulmshftlem  26432  reeff1o  26491  pilem2  26496  pilem3  26497  efif1olem2  26585  efopn  26700  cxpcn3lem  26790  cxpeq  26800  dcubic2  26887  quart  26904  xrlimcnp  27011  ftalem5  27120  ftalem7  27122  sgmnncl  27190  dvdsppwf1o  27229  musum  27234  perfect  27275  dchrptlem1  27308  dchrptlem2  27309  dchrpt  27311  bpos1lem  27326  lgsqrlem4  27393  lgsdchrval  27398  2sqblem  27475  dchrisumlem3  27535  chpdifbndlem2  27598  pntrsumbnd2  27611  pntpbnd1  27630  pntpbnd2  27631  pntpbnd  27632  pntibndlem2  27635  pntibndlem3  27636  pntleme  27652  pntlem3  27653  elno2  27699  sltval2  27701  noreson  27705  sltres  27707  noseponlem  27709  nolesgn2o  27716  nogesgn1o  27718  nodense  27737  nosupfv  27751  nosupres  27752  nosupbnd1lem3  27755  nosupbnd1lem5  27757  nosupbnd2lem1  27760  noinffv  27766  noinfres  27767  noinfbnd1lem3  27770  noinfbnd1lem5  27772  noinfbnd2lem1  27775  noetasuplem4  27781  noetainflem4  27785  noetalem2  27787  cuteq0  27877  cuteq1  27878  oldlim  27925  cofcutrtime  27961  cofss  27964  coiniss  27965  cutlt  27966  cutmax  27968  cutmin  27969  negsex  28075  negsfo  28085  norecdiv  28216  divs1  28229  precsexlem11  28241  precsex  28242  recsex  28243  elons2d  28282  n0ons  28339  dfnns2  28362  nohalf  28407  0reno  28429  readdscl  28431  axtgcont  28477  tgcgrxfr  28526  legid  28595  btwnleg  28596  leg0  28600  tghilberti1  28645  tglnpt2  28649  colline  28657  mirreu3  28662  isperp2  28723  colperpex  28741  lnopp2hpgb  28771  hpgerlem  28773  brbtwn  28914  brcgr  28915  brbtwn2  28920  axpasch  28956  axlowdimlem14  28970  axlowdim2  28975  axcontlem2  28980  axcontlem4  28982  axcontlem8  28986  axcontlem10  28988  axcontlem12  28990  fusgrn0degnn0  29517  friendshipgt3  30417  lpni  30499  isgrpoi  30517  vacn  30713  smcnlem  30716  nmosetn0  30784  nmoolb  30790  nmobndi  30794  nmoo0  30810  nmlno0lem  30812  isblo3i  30820  blo3i  30821  blocnilem  30823  ubthlem1  30889  minvecolem2  30894  minvecolem3  30895  minvecolem4c  30898  minvecolem4  30899  minvecolem5  30900  minvecolem6  30901  norm1exi  31269  occl  31323  spanval  31352  spancl  31355  shsval2i  31406  ococin  31427  pjoml6i  31608  nmopsetn0  31884  nmfnsetn0  31897  nmoplb  31926  nmfnlb  31943  nmop0  32005  nmfn0  32006  nmlnop0iALT  32014  nmopun  32033  nmcexi  32045  lnconi  32052  lnopcnbd  32055  lnfncnbd  32076  riesz3i  32081  riesz1  32084  cnlnadjlem2  32087  cnlnadjlem8  32093  cnlnadjlem9  32094  adjbd1o  32104  branmfn  32124  opsqrlem1  32159  pjnmopi  32167  strlem1  32269  stri  32276  hstri  32284  cvcon3  32303  cvnbtwn  32305  superpos  32373  shatomici  32377  atcvat4i  32416  mdsymlem2  32423  cdj1i  32452  cdj3i  32460  rexunirn  32511  foresf1o  32523  iundisjf  32602  aciunf1lem  32672  fnpreimac  32681  fgreu  32682  fcnvgreu  32683  xrge0infss  32764  ssnnssfz  32789  iundisjfi  32798  indf1ofs  32851  xreceu  32904  rexdiv  32908  isarchi3  33194  archirngz  33196  archiabllem2a  33201  0nellinds  33398  qtophaus  33835  reff  33838  locfinreflem  33839  cmpcref  33849  dispcmp  33858  tpr2rico  33911  pnfneige0  33950  qqhucn  33993  rrhre  34022  esumcst  34064  esumpcvgval  34079  dmsigagen  34145  rossros  34181  dya2icoseg  34279  dya2iocnrect  34283  dya2iocuni  34285  eulerpartlemgvv  34378  dstfrvunirn  34477  ballotlem4  34501  ballotlemic  34509  ballotlem1c  34510  ballotlemrc  34533  signsw0g  34571  signswmnd  34572  prodfzo03  34618  tgoldbachgt  34678  loop1cycl  35142  umgr2cycllem  35145  umgr2cycl  35146  subfacp1lem3  35187  erdsze2lem2  35209  cnpconn  35235  txpconn  35237  ptpconn  35238  indispconn  35239  connpconn  35240  cvxpconn  35247  cnllysconn  35250  cvmsss2  35279  cvmcov2  35280  cvmopnlem  35283  cvmliftlem14  35302  cvmliftlem15  35303  cvmlift2lem11  35318  cvmlift2lem12  35319  cvmlift2lem13  35320  cvmlift3lem2  35325  cvmlift3lem6  35329  cvmlift3lem9  35332  mthmi  35582  r1peuqusdeg1  35648  br8  35756  br6  35757  br4  35758  dfon2lem9  35792  wzel  35825  wsuclem  35826  wsuclb  35829  imagesset  35954  fvtransport  36033  brcolinear  36060  brsegle  36109  seglerflx  36113  seglemin  36114  btwnsegle  36118  fvray  36142  fvline  36145  hilbert1.1  36155  elhf2  36176  0hf  36178  nn0prpwlem  36323  nn0prpw  36324  fness  36350  fneref  36351  fnessref  36358  refssfne  36359  neibastop2lem  36361  fnemeet1  36367  tailfb  36378  filnetlem4  36382  limsucncmpi  36446  taupilemrplb  37321  relowlssretop  37364  rdgellim  37377  matunitlindflem2  37624  ptrecube  37627  poimirlem4  37631  poimirlem17  37644  poimirlem20  37647  poimirlem23  37650  poimirlem24  37651  poimirlem26  37653  poimirlem27  37654  poimirlem29  37656  poimirlem32  37659  heicant  37662  mblfinlem1  37664  mblfinlem2  37665  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  volsupnfl  37672  itg2addnclem  37678  itg2addnclem3  37680  itg2addnc  37681  ftc1anclem5  37704  unirep  37721  cover2  37722  indexa  37740  frinfm  37742  sdclem1  37750  fdc  37752  incsequz  37755  caushft  37768  istotbnd3  37778  0totbnd  37780  sstotbnd2  37781  sstotbnd  37782  sstotbnd3  37783  isbnd3  37791  ssbnd  37795  equivbnd  37797  prdsbnd  37800  prdstotbnd  37801  cntotbnd  37803  heibor1lem  37816  heiborlem1  37818  heiborlem3  37820  heiborlem6  37823  heiborlem8  37825  bfplem2  37830  rrncmslem  37839  iccbnd  37847  opidonOLD  37859  exidres  37885  isrngod  37905  isgrpda  37962  isdrngo2  37965  igenval  38068  igenidl  38070  prtlem10  38866  lshpnel2N  38986  lsmsat  39009  lssatomic  39012  lcvnbtwn  39026  lfl1  39071  eqlkr  39100  lshpkrlem1  39111  lshpkrex  39119  cvrcon3b  39278  cvrat4  39445  3dim3  39471  ps-2  39480  llni  39510  llnle  39520  lplni  39534  lplnle  39542  lplnexllnN  39566  lvoli  39577  lnatexN  39781  elpaddn0  39802  pclfinN  39902  lhprelat3N  40042  4atexlemex2  40073  4atex  40078  4atex2-0aOLDN  40080  4atex2-0cOLDN  40082  lautcvr  40094  cdleme0ex1N  40225  cdleme50rnlem  40546  cdleme50ex  40561  cdlemg1cex  40590  cdlemkid5  40937  cdlemk  40976  tendoex  40977  cdleml5N  40982  cdlemm10N  41120  dih1dimatlem0  41330  dihjat1lem  41430  dvh3dim2  41450  dvh3dim3N  41451  dochkr1  41480  dochkr1OLDN  41481  lcfrvalsnN  41543  lcfrlem27  41571  lcfrlem37  41581  lcfr  41587  mapd1o  41650  mapdpglem23  41696  hdmap11lem2  41844  primrootsunit1  42098  zdivgd  42372  resubeu  42407  fidomncyc  42545  nacsfix  42723  mzpcompact2lem  42762  eldioph  42769  diophrw  42770  diophin  42783  rexrabdioph  42805  rexzrexnn0  42815  eldioph4b  42822  rencldnfilem  42831  irrapxlem5  42837  irrapxlem6  42838  pell1234qrdich  42872  pell14qrdich  42880  infmrgelbi  42889  pellqrex  42890  pellfundre  42892  pellfundlb  42895  rmxynorm  42930  congrep  42985  acongrep  42992  jm2.27  43020  fnwe2lem2  43063  islssfgi  43084  hbtlem2  43136  hbtlem4  43138  hbtlem5  43140  dgraaub  43160  mpaaeu  43162  aaitgo  43174  unielss  43230  onexgt  43252  onexomgt  43253  onexlimgt  43255  onexoegt  43256  oaordnr  43309  omnord1  43318  oenord1  43329  oaomoencom  43330  oenass  43332  tfsconcatfv2  43353  tfsconcatrn  43355  tfsconcatb0  43357  ofoafo  43369  naddcnffo  43377  oaun3lem1  43387  naddwordnexlem4  43414  sucomisnotcard  43557  clsk1independent  44059  0elaxnul  45000  pwclaxpow  45001  prclaxpr  45002  uniclaxun  45003  omssaxinf2  45005  wfac8prim  45019  restuni3  45123  iinssd  45136  founiiun  45184  wessf1ornlem  45190  founiiun0  45195  unirnmap  45213  dstregt0  45293  uzfissfz  45337  rpgtrecnn  45391  rexabslelem  45429  infrnmptle  45434  infxrunb3rnmpt  45439  infxrpnf  45457  supminfxr  45475  rexanuz2nf  45503  iooiinicc  45555  iooiinioc  45569  uzubioo  45580  climsuse  45623  islptre  45634  limsuppnfdlem  45716  climinf3  45731  limsupmnfuzlem  45741  limsupre3lem  45747  limsupre3uzlem  45750  0cnv  45757  liminfreuzlem  45817  cnrefiisplem  45844  icccncfext  45902  cncficcgt0  45903  dvbdfbdioo  45945  ioodvbdlimc1lem1  45946  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  stoweidlem9  46024  stoweidlem14  46029  stoweidlem18  46033  stoweidlem21  46036  stoweidlem29  46044  stoweidlem34  46049  stoweidlem35  46050  stoweidlem39  46054  stoweidlem41  46056  stoweidlem45  46060  stoweidlem52  46067  stoweidlem55  46070  stoweidlem57  46072  stoweidlem60  46075  stirlinglem5  46093  stirlinglem13  46101  stirlinglem14  46102  fourierdlem16  46138  fourierdlem20  46142  fourierdlem21  46143  fourierdlem22  46144  fourierdlem25  46147  fourierdlem31  46153  fourierdlem39  46161  fourierdlem41  46163  fourierdlem42  46164  fourierdlem47  46168  fourierdlem48  46169  fourierdlem49  46170  fourierdlem51  46172  fourierdlem63  46184  fourierdlem64  46185  fourierdlem65  46186  fourierdlem77  46198  fourierdlem81  46202  fourierdlem83  46204  fourierdlem103  46224  fourierdlem104  46225  elaa2lem  46248  etransclem47  46296  qndenserrnbl  46310  ioorrnopnlem  46319  ioorrnopnxrlem  46321  intsaluni  46344  salgencntex  46358  subsaliuncllem  46372  sge0resplit  46421  sge0seq  46461  sge0reuz  46462  nnfoctbdjlem  46470  meaiininclem  46501  hoicvrrex  46571  ovnlecvr  46573  ovnlerp  46577  hoidmv1lelem2  46607  hoidmvlelem2  46611  hoidmvlelem3  46612  ovnhoilem1  46616  ovnlecvr2  46625  hoiqssbl  46640  ovolval4lem2  46665  ovolval5lem2  46668  ovnovollem1  46671  ovnovollem2  46672  iinhoiicclem  46688  smfinflem  46832  smflimsuplem7  46841  sprsymrelfolem2  47480  perfectALTV  47710  9gbo  47761  11gbo  47762  nnsum3primes4  47775  nnsum3primesprm  47777  ssnn0ssfz  48265  lincsumcl  48348  lincscmcl  48349  zlmodzxzldep  48421  ldepsnlinc  48425  line2ylem  48672  line2xlem  48674  sepfsepc  48825  lubsscl  48857  glbsscl  48858  aacllem  49320