Theorem rspcev 3576

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061

This theorem is referenced by:  rspcedvdw  3579  rspceb2dv  3580  rspceaimv  3582  rspc2ev  3589  rspc3ev  3593  rspceeqv  3599  reu6i  3686  rspesbca  3831  eliuni  4952  iuneqconst  4958  brralrspcev  5158  wefrc  5618  wereu2  5621  xpdifid  6126  frpomin  6298  onfr  6356  onelssex  6366  ordunidif  6367  eliman0  6871  dffv2  6929  elrnrexdm  7034  eldmrexrn  7036  elabrex  7188  elabrexg  7189  f1elima  7209  fliftfun  7258  fliftval  7262  f1oiso2  7298  sorpssuni  7677  sorpssint  7678  onssmin  7737  onminex  7747  fimaproj  8077  frxp3  8093  poseq  8100  tfrlem12  8320  seqomlem2  8382  oawordeulem  8481  oaass  8488  odi  8506  omass  8507  omeulem1  8509  oen0  8514  oelim2  8523  oeeulem  8529  nnawordex  8565  nnaordex2  8567  eldifsucnn  8592  cofon1  8600  cofon2  8601  naddcllem  8604  naddunif  8621  boxcutc  8881  0fi  8981  snfi  8982  rexdif1en  9087  findcard  9090  nnfi  9094  pssnn  9095  unfi  9097  onfin  9141  dif1ennnALT  9179  frfi  9187  fisupg  9190  nnsdomg  9201  pwfir  9219  prfi  9226  fissuni  9259  fipreima  9260  finsschain  9261  indexfi  9262  marypha1lem  9338  eqsup  9361  supmax  9373  fisup2g  9374  fisupcl  9375  supisoex  9380  infmin  9401  fiinfg  9406  fiinf2g  9407  wofib  9452  wemaplem2  9454  card2inf  9462  brwdom2  9480  cnfcom3clem  9616  ssttrcl  9626  ttrcltr  9627  trcl  9639  frmin  9663  r1ordg  9692  r1pwss  9698  tz9.12lem3  9703  tz9.12  9704  r1elwf  9710  tcrank  9798  scottex  9799  scott0  9800  isnumi  9860  onsdom  9910  ondomen  9949  infpwfien  9974  cardaleph  10001  infenaleph  10003  alephfplem4  10019  alephfp2  10021  dfac2b  10043  ackbij1lem18  10148  ackbij1  10149  cflem  10157  cflemOLD  10158  cflecard  10165  cfsuc  10169  cfflb  10171  cofsmo  10181  coftr  10185  fin23lem7  10228  fin23lem11  10229  enfin2i  10233  fin23lem26  10237  isf32lem5  10269  isf34lem4  10289  isfin1-3  10298  fin1a2lem7  10318  axdc3lem4  10365  ttukeylem7  10427  iunfo  10451  ficard  10477  pwcfsdom  10496  fpwwe2lem11  10554  wunex  10652  eltsk2g  10664  grur1  10733  axgroth6  10741  inaprc  10749  nqereu  10842  archnq  10893  genpnmax  10920  ltexpri  10956  prlem936  10960  recexpr  10964  supexpr  10967  negexsr  11015  recexsrlem  11016  recexsr  11020  supsrlem  11024  axrnegex  11075  axrrecex  11076  axpre-sup  11082  1re  11134  dedekind  11298  dedekindle  11299  cnegex  11316  cnegex2  11317  recex  11771  receu  11784  fiminre2  12092  cju  12143  nn2ge  12174  nominpos  12380  zdiv  12564  btwnz  12597  uzwo  12826  ublbneg  12848  lbzbi  12851  zsupss  12852  uzsupss  12855  rpnnen1lem1  12893  rpnnen1lem3  12894  rpnnen1lem4  12895  rpnnen1lem5  12896  z2ge  13115  qbtwnre  13116  qbtwnxr  13117  xralrple  13122  xrsupsslem  13224  xrinfmsslem  13225  supxrpnf  13235  icc0  13311  uzsup  13785  expnbnd  14157  expmulnbnd  14160  hashkf  14257  hashdom  14304  iswrdi  14442  rtrclreclem1  14982  rtrclreclem2  14984  rtrclreclem3  14985  01sqrex  15174  resqrex  15175  sqrtneg  15192  abs1m  15261  rexanuz  15271  rexuz3  15274  rexuzre  15278  sqreu  15286  o1lo1  15462  climconst  15468  rlimclim1  15470  climshftlem  15499  rlimo1  15542  lo1add  15552  lo1mul  15553  lo1le  15577  isercoll  15593  serf0  15606  zsum  15643  fsum  15645  fsumcvg3  15654  mertenslem1  15809  ntrivcvgn0  15823  ntrivcvgmullem  15826  zprod  15862  fprod  15866  fprodntriv  15867  dvdsval2  16184  dvds0lem  16195  dvds1lem  16196  dvds2lem  16197  odd2np1lem  16269  odd2np1  16270  opeo  16294  omeo  16295  divalglem9  16330  gcdcllem3  16430  lcmcllem  16525  qredeu  16587  exprmfct  16633  isprm5  16636  odzcllem  16722  reumodprminv  16734  modprm0  16735  nnnn0modprm0  16736  pythagtriplem19  16763  pcprmpw2  16812  pockthi  16837  infpnlem2  16841  vdwlem2  16912  vdwlem10  16920  vdwlem13  16923  ramub1lem1  16956  cshwrepswhash1  17032  imasleval  17464  mreexexlem3d  17571  mreexexlem4d  17572  iscatd  17598  cat1  18023  poslubd  18336  fpwipodrs  18465  ismgmid2  18595  mgmidsssn0  18599  gsumval2a  18612  ismndd  18683  isgrpd2  18888  isgrpd  18890  imasgrp2  18987  mhmmnd  18996  ghmgrp  18998  gaorber  19239  orbsta  19244  cayleyth  19346  pmtrdifel  19411  pmtrdifwrdel  19416  pmtrdifwrdel2  19417  psgnunilem2  19426  psgnunilem3  19427  psgnvalii  19440  pgpfi1  19526  sylow1lem3  19531  sylow1lem5  19533  pgpfi  19536  sylow2alem2  19549  efgredeu  19683  lt6abl  19826  pgpfac1lem3a  20009  pgpfac1lem3  20010  pgpfac1lem5  20012  pgpfaclem1  20014  pgpfaclem3  20016  ablfaclem2  20019  dvdsrmul  20302  dvdsr01  20309  irredrmul  20365  rhmdvdsr  20443  rgspnval  20547  rgspncl  20548  lspf  20927  lspval  20928  lssats2  20953  lspfixed  21085  lspsolvlem  21099  zringlpir  21424  pzriprnglem13  21450  zncyg  21505  cygth  21528  frlmup4  21758  aspval  21830  evlseu  22040  fiinbas  22898  topbas  22918  pptbas  22954  clsval  22983  elcls  23019  neiint  23050  neips  23059  opnneissb  23060  opnssneib  23061  innei  23071  neiptopnei  23078  restbas  23104  neitr  23126  pnfnei  23166  mnfnei  23167  lmconst  23207  iscnp4  23209  cncnpi  23224  cnconst2  23229  cnprest  23235  cnpdis  23239  nrmsep  23303  regsep2  23322  cmpcovf  23337  cmpsub  23346  cmpcld  23348  hauscmplem  23352  conncompid  23377  2ndci  23394  2ndcsb  23395  2ndc1stc  23397  1stcrest  23399  2ndcctbss  23401  2ndcdisj  23402  2ndcomap  23404  2ndcsep  23405  dis2ndc  23406  restlly  23429  islly2  23430  hausllycmp  23440  cldllycmp  23441  lly1stc  23442  dislly  23443  ssref  23458  refref  23459  finlocfin  23466  dissnlocfin  23475  locfindis  23476  llycmpkgen2  23496  cmpkgen  23497  1stckgenlem  23499  elptr  23519  ptbasfi  23527  neitx  23553  ptpjopn  23558  txcnp  23566  ptcnplem  23567  txlly  23582  txnlly  23583  txtube  23586  txcmplem1  23587  tx1stc  23596  txkgen  23598  xkococnlem  23605  txconn  23635  tgqtop  23658  kqreglem1  23687  kqreglem2  23688  kqnrmlem1  23689  kqnrmlem2  23690  reghmph  23739  nrmhmph  23740  fbssfi  23783  opnfbas  23788  isfil2  23802  fsubbas  23813  ssfg  23818  fgss2  23820  fbasrn  23830  filuni  23831  fgtr  23836  ssufl  23864  uffix  23867  elfm2  23894  elfm3  23896  imaelfm  23897  rnelfmlem  23898  rnelfm  23899  fmfnfmlem4  23903  fmfnfm  23904  fmco  23907  ufldom  23908  hausflim  23927  flimcls  23931  hauspwpwf1  23933  flffbas  23941  txflf  23952  fclscf  23971  fclsfnflim  23973  alexsubALTlem4  23996  alexsubALT  23997  tmdgsum2  24042  symgtgp  24052  subgntr  24053  opnsubg  24054  ghmcnp  24061  qustgpopn  24066  tsmsfbas  24074  tsmsxplem1  24099  ustexsym  24162  trust  24175  utoptop  24180  restutop  24183  restutopopn  24184  ustuqtop4  24190  utopsnneiplem  24193  iducn  24228  fmucnd  24237  cfilufg  24238  trcfilu  24239  neipcfilu  24241  imasdsf1olem  24319  blssps  24370  blss  24371  blssexps  24372  blssex  24373  ssblex  24374  blin2  24375  neibl  24447  blcld  24451  metss2  24458  stdbdmopn  24464  met1stc  24467  met2ndci  24468  metrest  24470  prdsxmslem2  24475  metcnp3  24486  metustexhalf  24502  metustfbas  24503  cfilucfil  24505  restmetu  24516  dscopn  24519  ngptgp  24582  nlmvscnlem1  24632  tgioo  24742  tgqioo  24746  xrsmopn  24759  zcld  24760  recld2  24761  zdis  24763  icccmplem1  24769  icccmplem2  24770  xmetdcn2  24784  addcnlem  24811  xrhmeo  24902  cnheibor  24912  cnllycmp  24913  lebnumlem3  24920  lebnum  24921  xlebnum  24922  lebnumii  24923  elpi1i  25004  ipcnlem1  25203  lmnn  25221  iscfil3  25231  cfilres  25254  flimcfil  25272  bcthlem4  25285  bcthlem5  25286  minveclem4c  25383  minveclem2  25384  minveclem3b  25386  minveclem3  25387  minveclem4  25390  minveclem6  25392  ivthlem2  25411  ivth  25413  ivthle  25415  ivthle2  25416  elovolmr  25435  ovolunlem1  25456  ovoliunlem2  25462  ovolicc1  25475  iundisj  25507  iunmbl2  25516  dyadmbllem  25558  volivth  25566  mbflimsup  25625  i1faddlem  25652  i1fmullem  25653  itg2lr  25689  itg2monolem1  25709  limcnlp  25837  ellimc3  25838  limcflf  25840  limciun  25853  rollelem  25951  c1lip1  25960  lhop1lem  25976  ply1divex  26100  ig1peu  26138  elply2  26159  coeeq  26190  plydivlem3  26261  plydivlem4  26262  elqaalem3  26287  qaa  26289  iaa  26291  aareccl  26292  aannenlem2  26295  aalioulem2  26299  aalioulem3  26300  aalioulem5  26302  aalioulem6  26303  aaliou  26304  aaliou2  26306  aaliou3lem8  26311  ulmshftlem  26356  reeff1o  26415  pilem2  26420  pilem3  26421  efif1olem2  26510  efopn  26625  cxpcn3lem  26715  cxpeq  26725  dcubic2  26812  quart  26829  xrlimcnp  26936  ftalem5  27045  ftalem7  27047  sgmnncl  27115  dvdsppwf1o  27154  musum  27159  perfect  27200  dchrptlem1  27233  dchrptlem2  27234  dchrpt  27236  bpos1lem  27251  lgsqrlem4  27318  lgsdchrval  27323  2sqblem  27400  dchrisumlem3  27460  chpdifbndlem2  27523  pntrsumbnd2  27536  pntpbnd1  27555  pntpbnd2  27556  pntpbnd  27557  pntibndlem2  27560  pntibndlem3  27561  pntleme  27577  pntlem3  27578  elno2  27624  ltsval2  27626  noreson  27630  ltsres  27632  noseponlem  27634  nolesgn2o  27641  nogesgn1o  27643  nodense  27662  nosupfv  27676  nosupres  27677  nosupbnd1lem3  27680  nosupbnd1lem5  27682  nosupbnd2lem1  27685  noinffv  27691  noinfres  27692  noinfbnd1lem3  27695  noinfbnd1lem5  27697  noinfbnd2lem1  27700  noetasuplem4  27706  noetainflem4  27710  noetalem2  27712  cuteq0  27813  cuteq1  27815  oldlim  27885  bdayiun  27913  cofcutrtime  27925  cofss  27928  coiniss  27929  cutlt  27930  cutmax  27932  cutmin  27933  negsex  28041  negsfo  28051  norecdiv  28188  divs1  28202  precsexlem11  28215  precsex  28216  recsex  28217  elons2d  28257  oncutlt  28262  n0on  28334  bdayn0sf1o  28368  dfnns2  28370  zsoring  28407  pw2recs  28436  halfcut  28456  0reno  28494  1reno  28495  readdscl  28497  axtgcont  28543  tgcgrxfr  28592  legid  28661  btwnleg  28662  leg0  28666  tghilberti1  28711  tglnpt2  28715  colline  28723  mirreu3  28728  isperp2  28789  colperpex  28807  lnopp2hpgb  28837  hpgerlem  28839  brbtwn  28974  brcgr  28975  brbtwn2  28980  axpasch  29016  axlowdimlem14  29030  axlowdim2  29035  axcontlem2  29040  axcontlem4  29042  axcontlem8  29046  axcontlem10  29048  axcontlem12  29050  fusgrn0degnn0  29575  friendshipgt3  30475  lpni  30557  isgrpoi  30575  vacn  30771  smcnlem  30774  nmosetn0  30842  nmoolb  30848  nmobndi  30852  nmoo0  30868  nmlno0lem  30870  isblo3i  30878  blo3i  30879  blocnilem  30881  ubthlem1  30947  minvecolem2  30952  minvecolem3  30953  minvecolem4c  30956  minvecolem4  30957  minvecolem5  30958  minvecolem6  30959  norm1exi  31327  occl  31381  spanval  31410  spancl  31413  shsval2i  31464  ococin  31485  pjoml6i  31666  nmopsetn0  31942  nmfnsetn0  31955  nmoplb  31984  nmfnlb  32001  nmop0  32063  nmfn0  32064  nmlnop0iALT  32072  nmopun  32091  nmcexi  32103  lnconi  32110  lnopcnbd  32113  lnfncnbd  32134  riesz3i  32139  riesz1  32142  cnlnadjlem2  32145  cnlnadjlem8  32151  cnlnadjlem9  32152  adjbd1o  32162  branmfn  32182  opsqrlem1  32217  pjnmopi  32225  strlem1  32327  stri  32334  hstri  32342  cvcon3  32361  cvnbtwn  32363  superpos  32431  shatomici  32435  atcvat4i  32474  mdsymlem2  32481  cdj1i  32510  cdj3i  32518  rexunirn  32568  foresf1o  32581  iundisjf  32666  aciunf1lem  32742  fnpreimac  32751  fgreu  32752  fcnvgreu  32753  xrge0infss  32842  ssnnssfz  32869  iundisjfi  32878  indf1ofs  32950  xreceu  33005  rexdiv  33009  isarchi3  33271  archirngz  33273  archiabllem2a  33278  0nellinds  33453  qtophaus  33995  reff  33998  locfinreflem  33999  cmpcref  34009  dispcmp  34018  tpr2rico  34071  pnfneige0  34110  qqhucn  34151  rrhre  34180  esumcst  34222  esumpcvgval  34237  dmsigagen  34303  rossros  34339  dya2icoseg  34436  dya2iocnrect  34440  dya2iocuni  34442  eulerpartlemgvv  34535  dstfrvunirn  34634  ballotlem4  34658  ballotlemic  34666  ballotlem1c  34667  ballotlemrc  34690  signsw0g  34715  signswmnd  34716  prodfzo03  34762  tgoldbachgt  34822  onvf1odlem4  35302  loop1cycl  35333  umgr2cycllem  35336  umgr2cycl  35337  subfacp1lem3  35378  erdsze2lem2  35400  cnpconn  35426  txpconn  35428  ptpconn  35429  indispconn  35430  connpconn  35431  cvxpconn  35438  cnllysconn  35441  cvmsss2  35470  cvmcov2  35471  cvmopnlem  35474  cvmliftlem14  35493  cvmliftlem15  35494  cvmlift2lem11  35509  cvmlift2lem12  35510  cvmlift2lem13  35511  cvmlift3lem2  35516  cvmlift3lem6  35520  cvmlift3lem9  35523  mthmi  35773  r1peuqusdeg1  35839  br8  35952  br6  35953  br4  35954  dfon2lem9  35985  wzel  36018  wsuclem  36019  wsuclb  36022  imagesset  36149  fvtransport  36228  brcolinear  36255  brsegle  36304  seglerflx  36308  seglemin  36309  btwnsegle  36313  fvray  36337  fvline  36340  hilbert1.1  36350  elhf2  36371  0hf  36373  nn0prpwlem  36518  nn0prpw  36519  fness  36545  fneref  36546  fnessref  36553  refssfne  36554  neibastop2lem  36556  fnemeet1  36562  tailfb  36573  filnetlem4  36577  limsucncmpi  36641  taupilemrplb  37527  relowlssretop  37570  rdgellim  37583  matunitlindflem2  37820  ptrecube  37823  poimirlem4  37827  poimirlem17  37840  poimirlem20  37843  poimirlem23  37846  poimirlem24  37847  poimirlem26  37849  poimirlem27  37850  poimirlem29  37852  poimirlem32  37855  heicant  37858  mblfinlem1  37860  mblfinlem2  37861  mblfinlem3  37862  mblfinlem4  37863  ismblfin  37864  volsupnfl  37868  itg2addnclem  37874  itg2addnclem3  37876  itg2addnc  37877  ftc1anclem5  37900  unirep  37917  cover2  37918  indexa  37936  frinfm  37938  sdclem1  37946  fdc  37948  incsequz  37951  caushft  37964  istotbnd3  37974  0totbnd  37976  sstotbnd2  37977  sstotbnd  37978  sstotbnd3  37979  isbnd3  37987  ssbnd  37991  equivbnd  37993  prdsbnd  37996  prdstotbnd  37997  cntotbnd  37999  heibor1lem  38012  heiborlem1  38014  heiborlem3  38016  heiborlem6  38019  heiborlem8  38021  bfplem2  38026  rrncmslem  38035  iccbnd  38043  opidonOLD  38055  exidres  38081  isrngod  38101  isgrpda  38158  isdrngo2  38161  igenval  38264  igenidl  38266  prtlem10  39147  lshpnel2N  39267  lsmsat  39290  lssatomic  39293  lcvnbtwn  39307  lfl1  39352  eqlkr  39381  lshpkrlem1  39392  lshpkrex  39400  cvrcon3b  39559  cvrat4  39725  3dim3  39751  ps-2  39760  llni  39790  llnle  39800  lplni  39814  lplnle  39822  lplnexllnN  39846  lvoli  39857  lnatexN  40061  elpaddn0  40082  pclfinN  40182  lhprelat3N  40322  4atexlemex2  40353  4atex  40358  4atex2-0aOLDN  40360  4atex2-0cOLDN  40362  lautcvr  40374  cdleme0ex1N  40505  cdleme50rnlem  40826  cdleme50ex  40841  cdlemg1cex  40870  cdlemkid5  41217  cdlemk  41256  tendoex  41257  cdleml5N  41262  cdlemm10N  41400  dih1dimatlem0  41610  dihjat1lem  41710  dvh3dim2  41730  dvh3dim3N  41731  dochkr1  41760  dochkr1OLDN  41761  lcfrvalsnN  41823  lcfrlem27  41851  lcfrlem37  41861  lcfr  41867  mapd1o  41930  mapdpglem23  41976  hdmap11lem2  42124  primrootsunit1  42373  zdivgd  42613  resubeu  42653  fidomncyc  42811  nacsfix  42975  mzpcompact2lem  43014  eldioph  43021  diophrw  43022  diophin  43035  rexrabdioph  43057  rexzrexnn0  43067  eldioph4b  43074  rencldnfilem  43083  irrapxlem5  43089  irrapxlem6  43090  pell1234qrdich  43124  pell14qrdich  43132  infmrgelbi  43141  pellqrex  43142  pellfundre  43144  pellfundlb  43147  rmxynorm  43181  congrep  43236  acongrep  43243  jm2.27  43271  fnwe2lem2  43314  islssfgi  43335  hbtlem2  43387  hbtlem4  43389  hbtlem5  43391  dgraaub  43411  mpaaeu  43413  aaitgo  43425  unielss  43481  onexgt  43503  onexomgt  43504  onexlimgt  43506  onexoegt  43507  oaordnr  43559  omnord1  43568  oenord1  43579  oaomoencom  43580  oenass  43582  tfsconcatfv2  43603  tfsconcatrn  43605  tfsconcatb0  43607  ofoafo  43619  naddcnffo  43627  oaun3lem1  43637  naddwordnexlem4  43664  sucomisnotcard  43806  clsk1independent  44308  0elaxnul  45245  pwclaxpow  45246  prclaxpr  45247  uniclaxun  45248  omssaxinf2  45250  wfac8prim  45264  restuni3  45383  iinssd  45396  founiiun  45444  wessf1ornlem  45450  founiiun0  45455  unirnmap  45473  dstregt0  45551  uzfissfz  45592  rpgtrecnn  45645  rexabslelem  45683  infrnmptle  45688  infxrunb3rnmpt  45693  infxrpnf  45711  supminfxr  45729  rexanuz2nf  45757  iooiinicc  45809  iooiinioc  45823  uzubioo  45832  climsuse  45875  islptre  45886  limsuppnfdlem  45966  climinf3  45981  limsupmnfuzlem  45991  limsupre3lem  45997  limsupre3uzlem  46000  0cnv  46007  liminfreuzlem  46067  cnrefiisplem  46094  icccncfext  46152  cncficcgt0  46153  dvbdfbdioo  46195  ioodvbdlimc1lem1  46196  ioodvbdlimc1lem2  46197  ioodvbdlimc2lem  46199  stoweidlem9  46274  stoweidlem14  46279  stoweidlem18  46283  stoweidlem21  46286  stoweidlem29  46294  stoweidlem34  46299  stoweidlem35  46300  stoweidlem39  46304  stoweidlem41  46306  stoweidlem45  46310  stoweidlem52  46317  stoweidlem55  46320  stoweidlem57  46322  stoweidlem60  46325  stirlinglem5  46343  stirlinglem13  46351  stirlinglem14  46352  fourierdlem16  46388  fourierdlem20  46392  fourierdlem21  46393  fourierdlem22  46394  fourierdlem25  46397  fourierdlem31  46403  fourierdlem39  46411  fourierdlem41  46413  fourierdlem42  46414  fourierdlem47  46418  fourierdlem48  46419  fourierdlem49  46420  fourierdlem51  46422  fourierdlem63  46434  fourierdlem64  46435  fourierdlem65  46436  fourierdlem77  46448  fourierdlem81  46452  fourierdlem83  46454  fourierdlem103  46474  fourierdlem104  46475  elaa2lem  46498  etransclem47  46546  qndenserrnbl  46560  ioorrnopnlem  46569  ioorrnopnxrlem  46571  intsaluni  46594  salgencntex  46608  subsaliuncllem  46622  sge0resplit  46671  sge0seq  46711  sge0reuz  46712  nnfoctbdjlem  46720  meaiininclem  46751  hoicvrrex  46821  ovnlecvr  46823  ovnlerp  46827  hoidmv1lelem2  46857  hoidmvlelem2  46861  hoidmvlelem3  46862  ovnhoilem1  46866  ovnlecvr2  46875  hoiqssbl  46890  ovolval4lem2  46915  ovolval5lem2  46918  ovnovollem1  46921  ovnovollem2  46922  iinhoiicclem  46938  smfinflem  47082  smflimsuplem7  47091  nthrucw  47151  sprsymrelfolem2  47760  perfectALTV  47990  9gbo  48041  11gbo  48042  nnsum3primes4  48055  nnsum3primesprm  48057  ssnn0ssfz  48616  lincsumcl  48698  lincscmcl  48699  zlmodzxzldep  48771  ldepsnlinc  48775  line2ylem  49018  line2xlem  49020  sepfsepc  49194  lubsscl  49226  glbsscl  49227  nelsubc3lem  49336  cnelsubclem  49869  aacllem  50067