Theorem rspcev 3578

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 3571	. 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  3581  rspceb2dv  3582  rspceaimv  3584  rspc2ev  3591  rspc3ev  3595  rspceeqv  3601  reu6i  3688  rspesbca  3833  eliuni  4954  iuneqconst  4960  brralrspcev  5160  wefrc  5626  wereu2  5629  xpdifid  6134  frpomin  6306  onfr  6364  onelssex  6374  ordunidif  6375  eliman0  6879  dffv2  6937  elrnrexdm  7043  eldmrexrn  7045  elabrex  7198  elabrexg  7199  f1elima  7219  fliftfun  7268  fliftval  7272  f1oiso2  7308  sorpssuni  7687  sorpssint  7688  onssmin  7747  onminex  7757  fimaproj  8087  frxp3  8103  poseq  8110  tfrlem12  8330  seqomlem2  8392  oawordeulem  8491  oaass  8498  odi  8516  omass  8517  omeulem1  8519  oen0  8524  oelim2  8533  oeeulem  8539  nnawordex  8575  nnaordex2  8577  eldifsucnn  8602  cofon1  8610  cofon2  8611  naddcllem  8614  naddunif  8631  boxcutc  8891  0fi  8991  snfi  8992  rexdif1en  9097  findcard  9100  nnfi  9104  pssnn  9105  unfi  9107  onfin  9151  dif1ennnALT  9189  frfi  9197  fisupg  9200  nnsdomg  9211  pwfir  9229  prfi  9236  fissuni  9269  fipreima  9270  finsschain  9271  indexfi  9272  marypha1lem  9348  eqsup  9371  supmax  9383  fisup2g  9384  fisupcl  9385  supisoex  9390  infmin  9411  fiinfg  9416  fiinf2g  9417  wofib  9462  wemaplem2  9464  card2inf  9472  brwdom2  9490  cnfcom3clem  9626  ssttrcl  9636  ttrcltr  9637  trcl  9649  frmin  9673  r1ordg  9702  r1pwss  9708  tz9.12lem3  9713  tz9.12  9714  r1elwf  9720  tcrank  9808  scottex  9809  scott0  9810  isnumi  9870  onsdom  9920  ondomen  9959  infpwfien  9984  cardaleph  10011  infenaleph  10013  alephfplem4  10029  alephfp2  10031  dfac2b  10053  ackbij1lem18  10158  ackbij1  10159  cflem  10167  cflemOLD  10168  cflecard  10175  cfsuc  10179  cfflb  10181  cofsmo  10191  coftr  10195  fin23lem7  10238  fin23lem11  10239  enfin2i  10243  fin23lem26  10247  isf32lem5  10279  isf34lem4  10299  isfin1-3  10308  fin1a2lem7  10328  axdc3lem4  10375  ttukeylem7  10437  iunfo  10461  ficard  10487  pwcfsdom  10506  fpwwe2lem11  10564  wunex  10662  eltsk2g  10674  grur1  10743  axgroth6  10751  inaprc  10759  nqereu  10852  archnq  10903  genpnmax  10930  ltexpri  10966  prlem936  10970  recexpr  10974  supexpr  10977  negexsr  11025  recexsrlem  11026  recexsr  11030  supsrlem  11034  axrnegex  11085  axrrecex  11086  axpre-sup  11092  1re  11144  dedekind  11308  dedekindle  11309  cnegex  11326  cnegex2  11327  recex  11781  receu  11794  fiminre2  12102  cju  12153  nn2ge  12184  nominpos  12390  zdiv  12574  btwnz  12607  uzwo  12836  ublbneg  12858  lbzbi  12861  zsupss  12862  uzsupss  12865  rpnnen1lem1  12903  rpnnen1lem3  12904  rpnnen1lem4  12905  rpnnen1lem5  12906  z2ge  13125  qbtwnre  13126  qbtwnxr  13127  xralrple  13132  xrsupsslem  13234  xrinfmsslem  13235  supxrpnf  13245  icc0  13321  uzsup  13795  expnbnd  14167  expmulnbnd  14170  hashkf  14267  hashdom  14314  iswrdi  14452  rtrclreclem1  14992  rtrclreclem2  14994  rtrclreclem3  14995  01sqrex  15184  resqrex  15185  sqrtneg  15202  abs1m  15271  rexanuz  15281  rexuz3  15284  rexuzre  15288  sqreu  15296  o1lo1  15472  climconst  15478  rlimclim1  15480  climshftlem  15509  rlimo1  15552  lo1add  15562  lo1mul  15563  lo1le  15587  isercoll  15603  serf0  15616  zsum  15653  fsum  15655  fsumcvg3  15664  mertenslem1  15819  ntrivcvgn0  15833  ntrivcvgmullem  15836  zprod  15872  fprod  15876  fprodntriv  15877  dvdsval2  16194  dvds0lem  16205  dvds1lem  16206  dvds2lem  16207  odd2np1lem  16279  odd2np1  16280  opeo  16304  omeo  16305  divalglem9  16340  gcdcllem3  16440  lcmcllem  16535  qredeu  16597  exprmfct  16643  isprm5  16646  odzcllem  16732  reumodprminv  16744  modprm0  16745  nnnn0modprm0  16746  pythagtriplem19  16773  pcprmpw2  16822  pockthi  16847  infpnlem2  16851  vdwlem2  16922  vdwlem10  16930  vdwlem13  16933  ramub1lem1  16966  cshwrepswhash1  17042  imasleval  17474  mreexexlem3d  17581  mreexexlem4d  17582  iscatd  17608  cat1  18033  poslubd  18346  fpwipodrs  18475  ismgmid2  18605  mgmidsssn0  18609  gsumval2a  18622  ismndd  18693  isgrpd2  18901  isgrpd  18903  imasgrp2  19000  mhmmnd  19009  ghmgrp  19011  gaorber  19252  orbsta  19257  cayleyth  19359  pmtrdifel  19424  pmtrdifwrdel  19429  pmtrdifwrdel2  19430  psgnunilem2  19439  psgnunilem3  19440  psgnvalii  19453  pgpfi1  19539  sylow1lem3  19544  sylow1lem5  19546  pgpfi  19549  sylow2alem2  19562  efgredeu  19696  lt6abl  19839  pgpfac1lem3a  20022  pgpfac1lem3  20023  pgpfac1lem5  20025  pgpfaclem1  20027  pgpfaclem3  20029  ablfaclem2  20032  dvdsrmul  20315  dvdsr01  20322  irredrmul  20378  rhmdvdsr  20456  rgspnval  20560  rgspncl  20561  lspf  20940  lspval  20941  lssats2  20966  lspfixed  21098  lspsolvlem  21112  zringlpir  21437  pzriprnglem13  21463  zncyg  21518  cygth  21541  frlmup4  21771  aspval  21843  evlseu  22053  fiinbas  22911  topbas  22931  pptbas  22967  clsval  22996  elcls  23032  neiint  23063  neips  23072  opnneissb  23073  opnssneib  23074  innei  23084  neiptopnei  23091  restbas  23117  neitr  23139  pnfnei  23179  mnfnei  23180  lmconst  23220  iscnp4  23222  cncnpi  23237  cnconst2  23242  cnprest  23248  cnpdis  23252  nrmsep  23316  regsep2  23335  cmpcovf  23350  cmpsub  23359  cmpcld  23361  hauscmplem  23365  conncompid  23390  2ndci  23407  2ndcsb  23408  2ndc1stc  23410  1stcrest  23412  2ndcctbss  23414  2ndcdisj  23415  2ndcomap  23417  2ndcsep  23418  dis2ndc  23419  restlly  23442  islly2  23443  hausllycmp  23453  cldllycmp  23454  lly1stc  23455  dislly  23456  ssref  23471  refref  23472  finlocfin  23479  dissnlocfin  23488  locfindis  23489  llycmpkgen2  23509  cmpkgen  23510  1stckgenlem  23512  elptr  23532  ptbasfi  23540  neitx  23566  ptpjopn  23571  txcnp  23579  ptcnplem  23580  txlly  23595  txnlly  23596  txtube  23599  txcmplem1  23600  tx1stc  23609  txkgen  23611  xkococnlem  23618  txconn  23648  tgqtop  23671  kqreglem1  23700  kqreglem2  23701  kqnrmlem1  23702  kqnrmlem2  23703  reghmph  23752  nrmhmph  23753  fbssfi  23796  opnfbas  23801  isfil2  23815  fsubbas  23826  ssfg  23831  fgss2  23833  fbasrn  23843  filuni  23844  fgtr  23849  ssufl  23877  uffix  23880  elfm2  23907  elfm3  23909  imaelfm  23910  rnelfmlem  23911  rnelfm  23912  fmfnfmlem4  23916  fmfnfm  23917  fmco  23920  ufldom  23921  hausflim  23940  flimcls  23944  hauspwpwf1  23946  flffbas  23954  txflf  23965  fclscf  23984  fclsfnflim  23986  alexsubALTlem4  24009  alexsubALT  24010  tmdgsum2  24055  symgtgp  24065  subgntr  24066  opnsubg  24067  ghmcnp  24074  qustgpopn  24079  tsmsfbas  24087  tsmsxplem1  24112  ustexsym  24175  trust  24188  utoptop  24193  restutop  24196  restutopopn  24197  ustuqtop4  24203  utopsnneiplem  24206  iducn  24241  fmucnd  24250  cfilufg  24251  trcfilu  24252  neipcfilu  24254  imasdsf1olem  24332  blssps  24383  blss  24384  blssexps  24385  blssex  24386  ssblex  24387  blin2  24388  neibl  24460  blcld  24464  metss2  24471  stdbdmopn  24477  met1stc  24480  met2ndci  24481  metrest  24483  prdsxmslem2  24488  metcnp3  24499  metustexhalf  24515  metustfbas  24516  cfilucfil  24518  restmetu  24529  dscopn  24532  ngptgp  24595  nlmvscnlem1  24645  tgioo  24755  tgqioo  24759  xrsmopn  24772  zcld  24773  recld2  24774  zdis  24776  icccmplem1  24782  icccmplem2  24783  xmetdcn2  24797  addcnlem  24824  xrhmeo  24915  cnheibor  24925  cnllycmp  24926  lebnumlem3  24933  lebnum  24934  xlebnum  24935  lebnumii  24936  elpi1i  25017  ipcnlem1  25216  lmnn  25234  iscfil3  25244  cfilres  25267  flimcfil  25285  bcthlem4  25298  bcthlem5  25299  minveclem4c  25396  minveclem2  25397  minveclem3b  25399  minveclem3  25400  minveclem4  25403  minveclem6  25405  ivthlem2  25424  ivth  25426  ivthle  25428  ivthle2  25429  elovolmr  25448  ovolunlem1  25469  ovoliunlem2  25475  ovolicc1  25488  iundisj  25520  iunmbl2  25529  dyadmbllem  25571  volivth  25579  mbflimsup  25638  i1faddlem  25665  i1fmullem  25666  itg2lr  25702  itg2monolem1  25722  limcnlp  25850  ellimc3  25851  limcflf  25853  limciun  25866  rollelem  25964  c1lip1  25973  lhop1lem  25989  ply1divex  26113  ig1peu  26151  elply2  26172  coeeq  26203  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  28557  tgcgrxfr  28606  legid  28675  btwnleg  28676  leg0  28680  tghilberti1  28725  tglnpt2  28729  colline  28737  mirreu3  28742  isperp2  28803  colperpex  28821  lnopp2hpgb  28851  hpgerlem  28853  brbtwn  28988  brcgr  28989  brbtwn2  28994  axpasch  29030  axlowdimlem14  29044  axlowdim2  29049  axcontlem2  29054  axcontlem4  29056  axcontlem8  29060  axcontlem10  29062  axcontlem12  29064  fusgrn0degnn0  29589  friendshipgt3  30489  lpni  30572  isgrpoi  30590  vacn  30786  smcnlem  30789  nmosetn0  30857  nmoolb  30863  nmobndi  30867  nmoo0  30883  nmlno0lem  30885  isblo3i  30893  blo3i  30894  blocnilem  30896  ubthlem1  30962  minvecolem2  30967  minvecolem3  30968  minvecolem4c  30971  minvecolem4  30972  minvecolem5  30973  minvecolem6  30974  norm1exi  31342  occl  31396  spanval  31425  spancl  31428  shsval2i  31479  ococin  31500  pjoml6i  31681  nmopsetn0  31957  nmfnsetn0  31970  nmoplb  31999  nmfnlb  32016  nmop0  32078  nmfn0  32079  nmlnop0iALT  32087  nmopun  32106  nmcexi  32118  lnconi  32125  lnopcnbd  32128  lnfncnbd  32149  riesz3i  32154  riesz1  32157  cnlnadjlem2  32160  cnlnadjlem8  32166  cnlnadjlem9  32167  adjbd1o  32177  branmfn  32197  opsqrlem1  32232  pjnmopi  32240  strlem1  32342  stri  32349  hstri  32357  cvcon3  32376  cvnbtwn  32378  superpos  32446  shatomici  32450  atcvat4i  32489  mdsymlem2  32496  cdj1i  32525  cdj3i  32533  rexunirn  32582  foresf1o  32595  iundisjf  32680  aciunf1lem  32756  fnpreimac  32764  fgreu  32765  fcnvgreu  32766  xrge0infss  32855  ssnnssfz  32882  iundisjfi  32891  indf1ofs  32963  xreceu  33018  rexdiv  33022  isarchi3  33285  archirngz  33287  archiabllem2a  33292  0nellinds  33467  qtophaus  34018  reff  34021  locfinreflem  34022  cmpcref  34032  dispcmp  34041  tpr2rico  34094  pnfneige0  34133  qqhucn  34174  rrhre  34203  esumcst  34245  esumpcvgval  34260  dmsigagen  34326  rossros  34362  dya2icoseg  34459  dya2iocnrect  34463  dya2iocuni  34465  eulerpartlemgvv  34558  dstfrvunirn  34657  ballotlem4  34681  ballotlemic  34689  ballotlem1c  34690  ballotlemrc  34713  signsw0g  34738  signswmnd  34739  prodfzo03  34785  tgoldbachgt  34845  onvf1odlem4  35326  loop1cycl  35357  umgr2cycllem  35360  umgr2cycl  35361  subfacp1lem3  35402  erdsze2lem2  35424  cnpconn  35450  txpconn  35452  ptpconn  35453  indispconn  35454  connpconn  35455  cvxpconn  35462  cnllysconn  35465  cvmsss2  35494  cvmcov2  35495  cvmopnlem  35498  cvmliftlem14  35517  cvmliftlem15  35518  cvmlift2lem11  35533  cvmlift2lem12  35534  cvmlift2lem13  35535  cvmlift3lem2  35540  cvmlift3lem6  35544  cvmlift3lem9  35547  mthmi  35797  r1peuqusdeg1  35863  br8  35976  br6  35977  br4  35978  dfon2lem9  36009  wzel  36042  wsuclem  36043  wsuclb  36046  imagesset  36173  fvtransport  36252  brcolinear  36279  brsegle  36328  seglerflx  36332  seglemin  36333  btwnsegle  36337  fvray  36361  fvline  36364  hilbert1.1  36374  elhf2  36395  0hf  36397  nn0prpwlem  36542  nn0prpw  36543  fness  36569  fneref  36570  fnessref  36577  refssfne  36578  neibastop2lem  36580  fnemeet1  36586  tailfb  36597  filnetlem4  36601  limsucncmpi  36665  taupilemrplb  37579  relowlssretop  37622  rdgellim  37635  matunitlindflem2  37872  ptrecube  37875  poimirlem4  37879  poimirlem17  37892  poimirlem20  37895  poimirlem23  37898  poimirlem24  37899  poimirlem26  37901  poimirlem27  37902  poimirlem29  37904  poimirlem32  37907  heicant  37910  mblfinlem1  37912  mblfinlem2  37913  mblfinlem3  37914  mblfinlem4  37915  ismblfin  37916  volsupnfl  37920  itg2addnclem  37926  itg2addnclem3  37928  itg2addnc  37929  ftc1anclem5  37952  unirep  37969  cover2  37970  indexa  37988  frinfm  37990  sdclem1  37998  fdc  38000  incsequz  38003  caushft  38016  istotbnd3  38026  0totbnd  38028  sstotbnd2  38029  sstotbnd  38030  sstotbnd3  38031  isbnd3  38039  ssbnd  38043  equivbnd  38045  prdsbnd  38048  prdstotbnd  38049  cntotbnd  38051  heibor1lem  38064  heiborlem1  38066  heiborlem3  38068  heiborlem6  38071  heiborlem8  38073  bfplem2  38078  rrncmslem  38087  iccbnd  38095  opidonOLD  38107  exidres  38133  isrngod  38153  isgrpda  38210  isdrngo2  38213  igenval  38316  igenidl  38318  prtlem10  39245  lshpnel2N  39365  lsmsat  39388  lssatomic  39391  lcvnbtwn  39405  lfl1  39450  eqlkr  39479  lshpkrlem1  39490  lshpkrex  39498  cvrcon3b  39657  cvrat4  39823  3dim3  39849  ps-2  39858  llni  39888  llnle  39898  lplni  39912  lplnle  39920  lplnexllnN  39944  lvoli  39955  lnatexN  40159  elpaddn0  40180  pclfinN  40280  lhprelat3N  40420  4atexlemex2  40451  4atex  40456  4atex2-0aOLDN  40458  4atex2-0cOLDN  40460  lautcvr  40472  cdleme0ex1N  40603  cdleme50rnlem  40924  cdleme50ex  40939  cdlemg1cex  40968  cdlemkid5  41315  cdlemk  41354  tendoex  41355  cdleml5N  41360  cdlemm10N  41498  dih1dimatlem0  41708  dihjat1lem  41808  dvh3dim2  41828  dvh3dim3N  41829  dochkr1  41858  dochkr1OLDN  41859  lcfrvalsnN  41921  lcfrlem27  41949  lcfrlem37  41959  lcfr  41965  mapd1o  42028  mapdpglem23  42074  hdmap11lem2  42222  primrootsunit1  42471  zdivgd  42711  resubeu  42751  fidomncyc  42909  nacsfix  43073  mzpcompact2lem  43112  eldioph  43119  diophrw  43120  diophin  43133  rexrabdioph  43155  rexzrexnn0  43165  eldioph4b  43172  rencldnfilem  43181  irrapxlem5  43187  irrapxlem6  43188  pell1234qrdich  43222  pell14qrdich  43230  infmrgelbi  43239  pellqrex  43240  pellfundre  43242  pellfundlb  43245  rmxynorm  43279  congrep  43334  acongrep  43341  jm2.27  43369  fnwe2lem2  43412  islssfgi  43433  hbtlem2  43485  hbtlem4  43487  hbtlem5  43489  dgraaub  43509  mpaaeu  43511  aaitgo  43523  unielss  43579  onexgt  43601  onexomgt  43602  onexlimgt  43604  onexoegt  43605  oaordnr  43657  omnord1  43666  oenord1  43677  oaomoencom  43678  oenass  43680  tfsconcatfv2  43701  tfsconcatrn  43703  tfsconcatb0  43705  ofoafo  43717  naddcnffo  43725  oaun3lem1  43735  naddwordnexlem4  43762  sucomisnotcard  43904  clsk1independent  44406  0elaxnul  45343  pwclaxpow  45344  prclaxpr  45345  uniclaxun  45346  omssaxinf2  45348  wfac8prim  45362  restuni3  45481  iinssd  45494  founiiun  45542  wessf1ornlem  45548  founiiun0  45553  unirnmap  45570  dstregt0  45648  uzfissfz  45689  rpgtrecnn  45742  rexabslelem  45780  infrnmptle  45785  infxrunb3rnmpt  45790  infxrpnf  45808  supminfxr  45826  rexanuz2nf  45854  iooiinicc  45906  iooiinioc  45920  uzubioo  45929  climsuse  45972  islptre  45983  limsuppnfdlem  46063  climinf3  46078  limsupmnfuzlem  46088  limsupre3lem  46094  limsupre3uzlem  46097  0cnv  46104  liminfreuzlem  46164  cnrefiisplem  46191  icccncfext  46249  cncficcgt0  46250  dvbdfbdioo  46292  ioodvbdlimc1lem1  46293  ioodvbdlimc1lem2  46294  ioodvbdlimc2lem  46296  stoweidlem9  46371  stoweidlem14  46376  stoweidlem18  46380  stoweidlem21  46383  stoweidlem29  46391  stoweidlem34  46396  stoweidlem35  46397  stoweidlem39  46401  stoweidlem41  46403  stoweidlem45  46407  stoweidlem52  46414  stoweidlem55  46417  stoweidlem57  46419  stoweidlem60  46422  stirlinglem5  46440  stirlinglem13  46448  stirlinglem14  46449  fourierdlem16  46485  fourierdlem20  46489  fourierdlem21  46490  fourierdlem22  46491  fourierdlem25  46494  fourierdlem31  46500  fourierdlem39  46508  fourierdlem41  46510  fourierdlem42  46511  fourierdlem47  46515  fourierdlem48  46516  fourierdlem49  46517  fourierdlem51  46519  fourierdlem63  46531  fourierdlem64  46532  fourierdlem65  46533  fourierdlem77  46545  fourierdlem81  46549  fourierdlem83  46551  fourierdlem103  46571  fourierdlem104  46572  elaa2lem  46595  etransclem47  46643  qndenserrnbl  46657  ioorrnopnlem  46666  ioorrnopnxrlem  46668  intsaluni  46691  salgencntex  46705  subsaliuncllem  46719  sge0resplit  46768  sge0seq  46808  sge0reuz  46809  nnfoctbdjlem  46817  meaiininclem  46848  hoicvrrex  46918  ovnlecvr  46920  ovnlerp  46924  hoidmv1lelem2  46954  hoidmvlelem2  46958  hoidmvlelem3  46959  ovnhoilem1  46963  ovnlecvr2  46972  hoiqssbl  46987  ovolval4lem2  47012  ovolval5lem2  47015  ovnovollem1  47018  ovnovollem2  47019  iinhoiicclem  47035  smfinflem  47179  smflimsuplem7  47188  nthrucw  47248  sprsymrelfolem2  47857  perfectALTV  48087  9gbo  48138  11gbo  48139  nnsum3primes4  48152  nnsum3primesprm  48154  ssnn0ssfz  48713  lincsumcl  48795  lincscmcl  48796  zlmodzxzldep  48868  ldepsnlinc  48872  line2ylem  49115  line2xlem  49117  sepfsepc  49291  lubsscl  49323  glbsscl  49324  nelsubc3lem  49433  cnelsubclem  49966  aacllem  50164