Theorem rspcev 3601

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 3594	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝜓 → ∃𝑥 ∈ 𝐵 𝜑))
5	4	imp 406	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061

This theorem is referenced by:  rspcedvdw  3604  rspceb2dv  3605  rspceaimv  3607  rspc2ev  3614  rspc3ev  3618  rspceeqv  3624  reu6i  3711  rspesbca  3856  eliuni  4973  iuneqconst  4979  brralrspcev  5179  wefrc  5648  wereu2  5651  xpdifid  6157  frpomin  6329  onfr  6391  onelssex  6401  ordunidif  6402  eliman0  6915  dffv2  6973  elrnrexdm  7078  eldmrexrn  7080  elabrex  7233  elabrexg  7234  elunirn2OLD  7244  f1elima  7255  fliftfun  7304  fliftval  7308  f1oiso2  7344  sorpssuni  7724  sorpssint  7725  onssmin  7784  onminex  7794  fimaproj  8132  frxp3  8148  poseq  8155  tfrlem12  8401  seqomlem2  8463  oawordeulem  8564  oaass  8571  odi  8589  omass  8590  omeulem1  8592  oen0  8596  oelim2  8605  oeeulem  8611  nnawordex  8647  nnaordex2  8649  eldifsucnn  8674  cofon1  8682  cofon2  8683  naddcllem  8686  naddunif  8703  boxcutc  8953  0fi  9054  snfi  9055  snfiOLD  9056  rexdif1en  9170  rexdif1enOLD  9171  findcard  9175  nnfi  9179  pssnn  9180  unfi  9183  onfin  9237  dif1ennnALT  9281  frfi  9291  fisupg  9294  nnsdomg  9305  nnsdomgOLD  9306  pwfir  9325  prfi  9333  fissuni  9367  fipreima  9368  finsschain  9369  indexfi  9370  marypha1lem  9443  eqsup  9466  supmax  9478  fisup2g  9479  fisupcl  9480  supisoex  9485  infmin  9506  fiinfg  9511  fiinf2g  9512  wofib  9557  wemaplem2  9559  card2inf  9567  brwdom2  9585  cnfcom3clem  9717  ssttrcl  9727  ttrcltr  9728  trcl  9740  frmin  9761  r1ordg  9790  r1pwss  9796  tz9.12lem3  9801  tz9.12  9802  r1elwf  9808  tcrank  9896  scottex  9897  scott0  9898  isnumi  9958  onsdom  10008  ondomen  10049  infpwfien  10074  cardaleph  10101  infenaleph  10103  alephfplem4  10119  alephfp2  10121  dfac2b  10143  ackbij1lem18  10248  ackbij1  10249  cflem  10257  cflemOLD  10258  cflecard  10265  cfsuc  10269  cfflb  10271  cofsmo  10281  coftr  10285  fin23lem7  10328  fin23lem11  10329  enfin2i  10333  fin23lem26  10337  isf32lem5  10369  isf34lem4  10389  isfin1-3  10398  fin1a2lem7  10418  axdc3lem4  10465  ttukeylem7  10527  iunfo  10551  ficard  10577  pwcfsdom  10595  fpwwe2lem11  10653  wunex  10751  eltsk2g  10763  grur1  10832  axgroth6  10840  inaprc  10848  nqereu  10941  archnq  10992  genpnmax  11019  ltexpri  11055  prlem936  11059  recexpr  11063  supexpr  11066  negexsr  11114  recexsrlem  11115  recexsr  11119  supsrlem  11123  axrnegex  11174  axrrecex  11175  axpre-sup  11181  1re  11233  dedekind  11396  dedekindle  11397  cnegex  11414  cnegex2  11415  recex  11867  receu  11880  fiminre2  12188  cju  12234  nn2ge  12265  nominpos  12476  zdiv  12661  btwnz  12694  uzwo  12925  ublbneg  12947  lbzbi  12950  zsupss  12951  uzsupss  12954  rpnnen1lem1  12992  rpnnen1lem3  12993  rpnnen1lem4  12994  rpnnen1lem5  12995  z2ge  13212  qbtwnre  13213  qbtwnxr  13214  xralrple  13219  xrsupsslem  13321  xrinfmsslem  13322  supxrpnf  13332  icc0  13408  uzsup  13878  expnbnd  14248  expmulnbnd  14251  hashkf  14348  hashdom  14395  iswrdi  14533  rtrclreclem1  15074  rtrclreclem2  15076  rtrclreclem3  15077  01sqrex  15266  resqrex  15267  sqrtneg  15284  abs1m  15352  rexanuz  15362  rexuz3  15365  rexuzre  15369  sqreu  15377  o1lo1  15551  climconst  15557  rlimclim1  15559  climshftlem  15588  rlimo1  15631  lo1add  15641  lo1mul  15642  lo1le  15666  isercoll  15682  serf0  15695  zsum  15732  fsum  15734  fsumcvg3  15743  mertenslem1  15898  ntrivcvgn0  15912  ntrivcvgmullem  15915  zprod  15951  fprod  15955  fprodntriv  15956  dvdsval2  16273  dvds0lem  16284  dvds1lem  16285  dvds2lem  16286  odd2np1lem  16357  odd2np1  16358  opeo  16382  omeo  16383  divalglem9  16418  gcdcllem3  16518  lcmcllem  16613  qredeu  16675  exprmfct  16721  isprm5  16724  odzcllem  16810  reumodprminv  16822  modprm0  16823  nnnn0modprm0  16824  pythagtriplem19  16851  pcprmpw2  16900  pockthi  16925  infpnlem2  16929  vdwlem2  17000  vdwlem10  17008  vdwlem13  17011  ramub1lem1  17044  cshwrepswhash1  17120  imasleval  17553  mreexexlem3d  17656  mreexexlem4d  17657  iscatd  17683  cat1  18108  poslubd  18421  fpwipodrs  18548  ismgmid2  18644  mgmidsssn0  18648  gsumval2a  18661  ismndd  18732  isgrpd2  18937  isgrpd  18939  imasgrp2  19036  mhmmnd  19045  ghmgrp  19047  gaorber  19289  orbsta  19294  cayleyth  19394  pmtrdifel  19459  pmtrdifwrdel  19464  pmtrdifwrdel2  19465  psgnunilem2  19474  psgnunilem3  19475  psgnvalii  19488  pgpfi1  19574  sylow1lem3  19579  sylow1lem5  19581  pgpfi  19584  sylow2alem2  19597  efgredeu  19731  lt6abl  19874  pgpfac1lem3a  20057  pgpfac1lem3  20058  pgpfac1lem5  20060  pgpfaclem1  20062  pgpfaclem3  20064  ablfaclem2  20067  dvdsrmul  20322  dvdsr01  20329  irredrmul  20385  rhmdvdsr  20466  rgspnval  20570  rgspncl  20571  lspf  20929  lspval  20930  lssats2  20955  lspfixed  21087  lspsolvlem  21101  zringlpir  21426  pzriprnglem13  21452  zncyg  21507  cygth  21530  frlmup4  21759  aspval  21831  evlseu  22039  fiinbas  22888  topbas  22908  pptbas  22944  clsval  22973  elcls  23009  neiint  23040  neips  23049  opnneissb  23050  opnssneib  23051  innei  23061  neiptopnei  23068  restbas  23094  neitr  23116  pnfnei  23156  mnfnei  23157  lmconst  23197  iscnp4  23199  cncnpi  23214  cnconst2  23219  cnprest  23225  cnpdis  23229  nrmsep  23293  regsep2  23312  cmpcovf  23327  cmpsub  23336  cmpcld  23338  hauscmplem  23342  conncompid  23367  2ndci  23384  2ndcsb  23385  2ndc1stc  23387  1stcrest  23389  2ndcctbss  23391  2ndcdisj  23392  2ndcomap  23394  2ndcsep  23395  dis2ndc  23396  restlly  23419  islly2  23420  hausllycmp  23430  cldllycmp  23431  lly1stc  23432  dislly  23433  ssref  23448  refref  23449  finlocfin  23456  dissnlocfin  23465  locfindis  23466  llycmpkgen2  23486  cmpkgen  23487  1stckgenlem  23489  elptr  23509  ptbasfi  23517  neitx  23543  ptpjopn  23548  txcnp  23556  ptcnplem  23557  txlly  23572  txnlly  23573  txtube  23576  txcmplem1  23577  tx1stc  23586  txkgen  23588  xkococnlem  23595  txconn  23625  tgqtop  23648  kqreglem1  23677  kqreglem2  23678  kqnrmlem1  23679  kqnrmlem2  23680  reghmph  23729  nrmhmph  23730  fbssfi  23773  opnfbas  23778  isfil2  23792  fsubbas  23803  ssfg  23808  fgss2  23810  fbasrn  23820  filuni  23821  fgtr  23826  ssufl  23854  uffix  23857  elfm2  23884  elfm3  23886  imaelfm  23887  rnelfmlem  23888  rnelfm  23889  fmfnfmlem4  23893  fmfnfm  23894  fmco  23897  ufldom  23898  hausflim  23917  flimcls  23921  hauspwpwf1  23923  flffbas  23931  txflf  23942  fclscf  23961  fclsfnflim  23963  alexsubALTlem4  23986  alexsubALT  23987  tmdgsum2  24032  symgtgp  24042  subgntr  24043  opnsubg  24044  ghmcnp  24051  qustgpopn  24056  tsmsfbas  24064  tsmsxplem1  24089  ustexsym  24152  trust  24166  utoptop  24171  restutop  24174  restutopopn  24175  ustuqtop4  24181  utopsnneiplem  24184  iducn  24219  fmucnd  24228  cfilufg  24229  trcfilu  24230  neipcfilu  24232  imasdsf1olem  24310  blssps  24361  blss  24362  blssexps  24363  blssex  24364  ssblex  24365  blin2  24366  neibl  24438  blcld  24442  metss2  24449  stdbdmopn  24455  met1stc  24458  met2ndci  24459  metrest  24461  prdsxmslem2  24466  metcnp3  24477  metustexhalf  24493  metustfbas  24494  cfilucfil  24496  restmetu  24507  dscopn  24510  ngptgp  24573  nlmvscnlem1  24623  tgioo  24733  tgqioo  24737  xrsmopn  24750  zcld  24751  recld2  24752  zdis  24754  icccmplem1  24760  icccmplem2  24761  xmetdcn2  24775  addcnlem  24802  xrhmeo  24893  cnheibor  24903  cnllycmp  24904  lebnumlem3  24911  lebnum  24912  xlebnum  24913  lebnumii  24914  elpi1i  24995  ipcnlem1  25195  lmnn  25213  iscfil3  25223  cfilres  25246  flimcfil  25264  bcthlem4  25277  bcthlem5  25278  minveclem4c  25375  minveclem2  25376  minveclem3b  25378  minveclem3  25379  minveclem4  25382  minveclem6  25384  ivthlem2  25403  ivth  25405  ivthle  25407  ivthle2  25408  elovolmr  25427  ovolunlem1  25448  ovoliunlem2  25454  ovolicc1  25467  iundisj  25499  iunmbl2  25508  dyadmbllem  25550  volivth  25558  mbflimsup  25617  i1faddlem  25644  i1fmullem  25645  itg2lr  25681  itg2monolem1  25701  limcnlp  25829  ellimc3  25830  limcflf  25832  limciun  25845  rollelem  25943  c1lip1  25952  lhop1lem  25968  ply1divex  26092  ig1peu  26130  elply2  26151  coeeq  26182  plydivlem3  26253  plydivlem4  26254  elqaalem3  26279  qaa  26281  iaa  26283  aareccl  26284  aannenlem2  26287  aalioulem2  26291  aalioulem3  26292  aalioulem5  26294  aalioulem6  26295  aaliou  26296  aaliou2  26298  aaliou3lem8  26303  ulmshftlem  26348  reeff1o  26407  pilem2  26412  pilem3  26413  efif1olem2  26502  efopn  26617  cxpcn3lem  26707  cxpeq  26717  dcubic2  26804  quart  26821  xrlimcnp  26928  ftalem5  27037  ftalem7  27039  sgmnncl  27107  dvdsppwf1o  27146  musum  27151  perfect  27192  dchrptlem1  27225  dchrptlem2  27226  dchrpt  27228  bpos1lem  27243  lgsqrlem4  27310  lgsdchrval  27315  2sqblem  27392  dchrisumlem3  27452  chpdifbndlem2  27515  pntrsumbnd2  27528  pntpbnd1  27547  pntpbnd2  27548  pntpbnd  27549  pntibndlem2  27552  pntibndlem3  27553  pntleme  27569  pntlem3  27570  elno2  27616  sltval2  27618  noreson  27622  sltres  27624  noseponlem  27626  nolesgn2o  27633  nogesgn1o  27635  nodense  27654  nosupfv  27668  nosupres  27669  nosupbnd1lem3  27672  nosupbnd1lem5  27674  nosupbnd2lem1  27677  noinffv  27683  noinfres  27684  noinfbnd1lem3  27687  noinfbnd1lem5  27689  noinfbnd2lem1  27692  noetasuplem4  27698  noetainflem4  27702  noetalem2  27704  cuteq0  27794  cuteq1  27795  oldlim  27842  cofcutrtime  27878  cofss  27881  coiniss  27882  cutlt  27883  cutmax  27885  cutmin  27886  negsex  27992  negsfo  28002  norecdiv  28133  divs1  28146  precsexlem11  28158  precsex  28159  recsex  28160  elons2d  28199  n0ons  28256  dfnns2  28279  nohalf  28324  0reno  28346  readdscl  28348  axtgcont  28394  tgcgrxfr  28443  legid  28512  btwnleg  28513  leg0  28517  tghilberti1  28562  tglnpt2  28566  colline  28574  mirreu3  28579  isperp2  28640  colperpex  28658  lnopp2hpgb  28688  hpgerlem  28690  brbtwn  28824  brcgr  28825  brbtwn2  28830  axpasch  28866  axlowdimlem14  28880  axlowdim2  28885  axcontlem2  28890  axcontlem4  28892  axcontlem8  28896  axcontlem10  28898  axcontlem12  28900  fusgrn0degnn0  29425  friendshipgt3  30325  lpni  30407  isgrpoi  30425  vacn  30621  smcnlem  30624  nmosetn0  30692  nmoolb  30698  nmobndi  30702  nmoo0  30718  nmlno0lem  30720  isblo3i  30728  blo3i  30729  blocnilem  30731  ubthlem1  30797  minvecolem2  30802  minvecolem3  30803  minvecolem4c  30806  minvecolem4  30807  minvecolem5  30808  minvecolem6  30809  norm1exi  31177  occl  31231  spanval  31260  spancl  31263  shsval2i  31314  ococin  31335  pjoml6i  31516  nmopsetn0  31792  nmfnsetn0  31805  nmoplb  31834  nmfnlb  31851  nmop0  31913  nmfn0  31914  nmlnop0iALT  31922  nmopun  31941  nmcexi  31953  lnconi  31960  lnopcnbd  31963  lnfncnbd  31984  riesz3i  31989  riesz1  31992  cnlnadjlem2  31995  cnlnadjlem8  32001  cnlnadjlem9  32002  adjbd1o  32012  branmfn  32032  opsqrlem1  32067  pjnmopi  32075  strlem1  32177  stri  32184  hstri  32192  cvcon3  32211  cvnbtwn  32213  superpos  32281  shatomici  32285  atcvat4i  32324  mdsymlem2  32331  cdj1i  32360  cdj3i  32368  rexunirn  32419  foresf1o  32431  iundisjf  32516  aciunf1lem  32586  fnpreimac  32595  fgreu  32596  fcnvgreu  32597  xrge0infss  32683  ssnnssfz  32710  iundisjfi  32719  indf1ofs  32789  xreceu  32842  rexdiv  32846  isarchi3  33131  archirngz  33133  archiabllem2a  33138  0nellinds  33331  qtophaus  33813  reff  33816  locfinreflem  33817  cmpcref  33827  dispcmp  33836  tpr2rico  33889  pnfneige0  33928  qqhucn  33969  rrhre  33998  esumcst  34040  esumpcvgval  34055  dmsigagen  34121  rossros  34157  dya2icoseg  34255  dya2iocnrect  34259  dya2iocuni  34261  eulerpartlemgvv  34354  dstfrvunirn  34453  ballotlem4  34477  ballotlemic  34485  ballotlem1c  34486  ballotlemrc  34509  signsw0g  34534  signswmnd  34535  prodfzo03  34581  tgoldbachgt  34641  loop1cycl  35105  umgr2cycllem  35108  umgr2cycl  35109  subfacp1lem3  35150  erdsze2lem2  35172  cnpconn  35198  txpconn  35200  ptpconn  35201  indispconn  35202  connpconn  35203  cvxpconn  35210  cnllysconn  35213  cvmsss2  35242  cvmcov2  35243  cvmopnlem  35246  cvmliftlem14  35265  cvmliftlem15  35266  cvmlift2lem11  35281  cvmlift2lem12  35282  cvmlift2lem13  35283  cvmlift3lem2  35288  cvmlift3lem6  35292  cvmlift3lem9  35295  mthmi  35545  r1peuqusdeg1  35611  br8  35719  br6  35720  br4  35721  dfon2lem9  35755  wzel  35788  wsuclem  35789  wsuclb  35792  imagesset  35917  fvtransport  35996  brcolinear  36023  brsegle  36072  seglerflx  36076  seglemin  36077  btwnsegle  36081  fvray  36105  fvline  36108  hilbert1.1  36118  elhf2  36139  0hf  36141  nn0prpwlem  36286  nn0prpw  36287  fness  36313  fneref  36314  fnessref  36321  refssfne  36322  neibastop2lem  36324  fnemeet1  36330  tailfb  36341  filnetlem4  36345  limsucncmpi  36409  taupilemrplb  37284  relowlssretop  37327  rdgellim  37340  matunitlindflem2  37587  ptrecube  37590  poimirlem4  37594  poimirlem17  37607  poimirlem20  37610  poimirlem23  37613  poimirlem24  37614  poimirlem26  37616  poimirlem27  37617  poimirlem29  37619  poimirlem32  37622  heicant  37625  mblfinlem1  37627  mblfinlem2  37628  mblfinlem3  37629  mblfinlem4  37630  ismblfin  37631  volsupnfl  37635  itg2addnclem  37641  itg2addnclem3  37643  itg2addnc  37644  ftc1anclem5  37667  unirep  37684  cover2  37685  indexa  37703  frinfm  37705  sdclem1  37713  fdc  37715  incsequz  37718  caushft  37731  istotbnd3  37741  0totbnd  37743  sstotbnd2  37744  sstotbnd  37745  sstotbnd3  37746  isbnd3  37754  ssbnd  37758  equivbnd  37760  prdsbnd  37763  prdstotbnd  37764  cntotbnd  37766  heibor1lem  37779  heiborlem1  37781  heiborlem3  37783  heiborlem6  37786  heiborlem8  37788  bfplem2  37793  rrncmslem  37802  iccbnd  37810  opidonOLD  37822  exidres  37848  isrngod  37868  isgrpda  37925  isdrngo2  37928  igenval  38031  igenidl  38033  prtlem10  38829  lshpnel2N  38949  lsmsat  38972  lssatomic  38975  lcvnbtwn  38989  lfl1  39034  eqlkr  39063  lshpkrlem1  39074  lshpkrex  39082  cvrcon3b  39241  cvrat4  39408  3dim3  39434  ps-2  39443  llni  39473  llnle  39483  lplni  39497  lplnle  39505  lplnexllnN  39529  lvoli  39540  lnatexN  39744  elpaddn0  39765  pclfinN  39865  lhprelat3N  40005  4atexlemex2  40036  4atex  40041  4atex2-0aOLDN  40043  4atex2-0cOLDN  40045  lautcvr  40057  cdleme0ex1N  40188  cdleme50rnlem  40509  cdleme50ex  40524  cdlemg1cex  40553  cdlemkid5  40900  cdlemk  40939  tendoex  40940  cdleml5N  40945  cdlemm10N  41083  dih1dimatlem0  41293  dihjat1lem  41393  dvh3dim2  41413  dvh3dim3N  41414  dochkr1  41443  dochkr1OLDN  41444  lcfrvalsnN  41506  lcfrlem27  41534  lcfrlem37  41544  lcfr  41550  mapd1o  41613  mapdpglem23  41659  hdmap11lem2  41807  primrootsunit1  42056  zdivgd  42333  resubeu  42367  fidomncyc  42505  nacsfix  42682  mzpcompact2lem  42721  eldioph  42728  diophrw  42729  diophin  42742  rexrabdioph  42764  rexzrexnn0  42774  eldioph4b  42781  rencldnfilem  42790  irrapxlem5  42796  irrapxlem6  42797  pell1234qrdich  42831  pell14qrdich  42839  infmrgelbi  42848  pellqrex  42849  pellfundre  42851  pellfundlb  42854  rmxynorm  42889  congrep  42944  acongrep  42951  jm2.27  42979  fnwe2lem2  43022  islssfgi  43043  hbtlem2  43095  hbtlem4  43097  hbtlem5  43099  dgraaub  43119  mpaaeu  43121  aaitgo  43133  unielss  43189  onexgt  43211  onexomgt  43212  onexlimgt  43214  onexoegt  43215  oaordnr  43267  omnord1  43276  oenord1  43287  oaomoencom  43288  oenass  43290  tfsconcatfv2  43311  tfsconcatrn  43313  tfsconcatb0  43315  ofoafo  43327  naddcnffo  43335  oaun3lem1  43345  naddwordnexlem4  43372  sucomisnotcard  43515  clsk1independent  44017  0elaxnul  44956  pwclaxpow  44957  prclaxpr  44958  uniclaxun  44959  omssaxinf2  44961  wfac8prim  44975  restuni3  45090  iinssd  45103  founiiun  45151  wessf1ornlem  45157  founiiun0  45162  unirnmap  45180  dstregt0  45258  uzfissfz  45301  rpgtrecnn  45355  rexabslelem  45393  infrnmptle  45398  infxrunb3rnmpt  45403  infxrpnf  45421  supminfxr  45439  rexanuz2nf  45467  iooiinicc  45519  iooiinioc  45533  uzubioo  45542  climsuse  45585  islptre  45596  limsuppnfdlem  45678  climinf3  45693  limsupmnfuzlem  45703  limsupre3lem  45709  limsupre3uzlem  45712  0cnv  45719  liminfreuzlem  45779  cnrefiisplem  45806  icccncfext  45864  cncficcgt0  45865  dvbdfbdioo  45907  ioodvbdlimc1lem1  45908  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  stoweidlem9  45986  stoweidlem14  45991  stoweidlem18  45995  stoweidlem21  45998  stoweidlem29  46006  stoweidlem34  46011  stoweidlem35  46012  stoweidlem39  46016  stoweidlem41  46018  stoweidlem45  46022  stoweidlem52  46029  stoweidlem55  46032  stoweidlem57  46034  stoweidlem60  46037  stirlinglem5  46055  stirlinglem13  46063  stirlinglem14  46064  fourierdlem16  46100  fourierdlem20  46104  fourierdlem21  46105  fourierdlem22  46106  fourierdlem25  46109  fourierdlem31  46115  fourierdlem39  46123  fourierdlem41  46125  fourierdlem42  46126  fourierdlem47  46130  fourierdlem48  46131  fourierdlem49  46132  fourierdlem51  46134  fourierdlem63  46146  fourierdlem64  46147  fourierdlem65  46148  fourierdlem77  46160  fourierdlem81  46164  fourierdlem83  46166  fourierdlem103  46186  fourierdlem104  46187  elaa2lem  46210  etransclem47  46258  qndenserrnbl  46272  ioorrnopnlem  46281  ioorrnopnxrlem  46283  intsaluni  46306  salgencntex  46320  subsaliuncllem  46334  sge0resplit  46383  sge0seq  46423  sge0reuz  46424  nnfoctbdjlem  46432  meaiininclem  46463  hoicvrrex  46533  ovnlecvr  46535  ovnlerp  46539  hoidmv1lelem2  46569  hoidmvlelem2  46573  hoidmvlelem3  46574  ovnhoilem1  46578  ovnlecvr2  46587  hoiqssbl  46602  ovolval4lem2  46627  ovolval5lem2  46630  ovnovollem1  46633  ovnovollem2  46634  iinhoiicclem  46650  smfinflem  46794  smflimsuplem7  46803  sprsymrelfolem2  47455  perfectALTV  47685  9gbo  47736  11gbo  47737  nnsum3primes4  47750  nnsum3primesprm  47752  ssnn0ssfz  48272  lincsumcl  48355  lincscmcl  48356  zlmodzxzldep  48428  ldepsnlinc  48432  line2ylem  48679  line2xlem  48681  sepfsepc  48850  lubsscl  48882  glbsscl  48883  nelsubc3lem  48985  cnelsubclem  49428  aacllem  49613