Theorem rspcev 3581

Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2176, ax-11 2192, ax-12 2213. (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 23	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ 𝐵)
2		rspcv.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	adantl 486	. . 3 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓))
4	1, 3	rspcedv 3574	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝜓 → ∃𝑥 ∈ 𝐵 𝜑))
5	4	imp 411	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090

This theorem is referenced by:  rspcedvdw  3584  rspceaimv  3587  rspc2ev  3594  rspc3ev  3598  rspceeqv  3604  reu6i  3691  rspesbca  3834  eliuni  4962  iuneqconst  4968  brralrspcev  5171  wefrc  5655  wereu2  5658  xpdifid  6165  xpdifcnvepel  6166  frpomin  6341  onfr  6400  onelssex  6410  ordunidif  6411  eliman0  6918  dffv2  6976  elrnrexdm  7084  eldmrexrn  7086  elabrex  7240  elabrexg  7241  f1elima  7261  fliftfun  7310  fliftval  7314  f1oiso2  7350  sorpssuni  7729  sorpssint  7730  onssmin  7787  onminex  7797  fimaproj  8127  frxp3  8143  poseq  8150  tfrlem12  8372  seqomlem2  8434  oawordeulem  8535  oaass  8542  odi  8560  omass  8561  omeulem1  8563  oen0  8568  oelim2  8577  oeeulem  8583  nnawordex  8619  nnaordex2  8621  eldifsucnn  8646  cofon1  8654  cofon2  8655  naddcllem  8658  naddunif  8676  boxcutc  8935  0fi  9035  snfi  9036  rexdif1en  9141  findcard  9144  nnfi  9148  pssnn  9149  unfi  9151  onfin  9195  dif1ennnALT  9233  frfi  9241  fisupg  9244  nnsdomg  9255  pwfir  9272  prfi  9279  fissuni  9310  fipreima  9311  finsschain  9312  indexfi  9313  marypha1lem  9389  eqsup  9412  supmax  9424  fisup2g  9425  fisupcl  9426  supisoex  9431  infmin  9452  fiinfg  9457  fiinf2g  9458  wofib  9503  wemaplem2  9505  card2inf  9513  brwdom2  9531  cnfcom3clem  9670  ssttrcl  9680  ttrcltr  9681  trcl  9693  frmin  9717  r1ordg  9746  r1pwss  9752  tz9.12lem3  9757  tz9.12  9758  r1elwf  9764  tcrank  9852  scottex  9855  scott0  9856  isnumi  9928  onsdom  9978  ondomen  10017  infpwfien  10042  cardaleph  10069  infenaleph  10071  alephfplem4  10087  alephfp2  10089  dfac2b  10110  ackbij1lem18  10215  ackbij1  10216  cflem  10224  cflecard  10231  cfsuc  10236  cfflb  10238  cofsmo  10248  coftr  10252  fin23lem7  10295  fin23lem11  10296  enfin2i  10300  fin23lem26  10304  isf32lem5  10336  isf34lem4  10356  isfin1-3  10365  fin1a2lem7  10385  axdc3lem4  10432  ttukeylem7  10494  iunfo  10518  ficard  10544  pwcfsdom  10563  fpwwe2lem11  10621  wunex  10719  eltsk2g  10731  grur1  10800  axgroth6  10808  inaprc  10816  nqereu  10909  archnq  10960  genpnmax  10987  ltexpri  11023  prlem936  11027  recexpr  11031  supexpr  11034  negexsr  11082  recexsrlem  11083  recexsr  11087  supsrlem  11091  axrnegex  11142  axrrecex  11143  axpre-sup  11149  1re  11203  dedekind  11368  dedekindle  11369  cnegex  11386  cnegex2  11387  recex  11841  receu  11854  fiminre2  12158  cju  12209  nn2ge  12258  nominpos  12476  zdiv  12661  btwnz  12694  uzwo  12930  ublbneg  12952  lbzbi  12955  zsupss  12956  uzsupss  12959  rpnnen1lem1  12997  rpnnen1lem3  12998  rpnnen1lem4  12999  rpnnen1lem5  13000  z2ge  13219  qbtwnre  13220  qbtwnxr  13221  xralrple  13226  xrsupsslem  13328  xrinfmsslem  13329  supxrpnf  13339  icc0  13415  uzsup  13892  expnbnd  14264  expmulnbnd  14267  hashkf  14364  hashdom  14411  iswrdi  14550  rtrclreclem1  15090  rtrclreclem2  15092  rtrclreclem3  15093  01sqrex  15296  resqrex  15297  sqrtneg  15314  abs1m  15383  rexanuz  15393  rexuz3  15396  rexuzre  15400  sqreu  15408  o1lo1  15584  climconst  15590  rlimclim1  15592  climshftlem  15621  rlimo1  15664  lo1add  15674  lo1mul  15675  lo1le  15699  isercoll  15715  serf0  15728  zsum  15765  fsum  15767  fsumcvg3  15776  mertenslem1  15934  ntrivcvgn0  15948  ntrivcvgmullem  15951  zprod  15987  fprod  15991  fprodntriv  15992  dvdsval2  16308  dvds0lem  16319  dvds1lem  16320  dvds2lem  16321  odd2np1lem  16393  odd2np1  16394  opeo  16418  omeo  16419  divalglem9  16454  gcdcllem3  16554  lcmcllem  16649  qredeu  16711  exprmfct  16758  isprm5  16761  odzcllem  16847  reumodprminv  16859  modprm0  16860  nnnn0modprm0  16861  pythagtriplem19  16888  pcprmpw2  16937  pockthi  16962  infpnlem2  16966  vdwlem2  17037  vdwlem10  17045  vdwlem13  17048  ramub1lem1  17081  cshwrepswhash1  17157  imasleval  17590  mreexexlem3d  17697  mreexexlem4d  17698  iscatd  17724  cat1  18149  poslubd  18462  fpwipodrs  18591  ismgmid2  18721  mgmidsssn0  18725  gsumval2a  18738  ismndd  18809  isgrpd2  19018  isgrpd  19020  imasgrp2  19116  mhmmnd  19125  ghmgrp  19127  gaorber  19373  orbsta  19378  cayleyth  19480  pmtrdifel  19545  pmtrdifwrdel  19550  pmtrdifwrdel2  19551  psgnunilem2  19560  psgnunilem3  19561  psgnvalii  19574  pgpfi1  19660  sylow1lem3  19665  sylow1lem5  19667  pgpfi  19670  sylow2alem2  19683  efgredeu  19817  lt6abl  19960  pgpfac1lem3a  20143  pgpfac1lem3  20144  pgpfac1lem5  20146  pgpfaclem1  20148  pgpfaclem3  20150  ablfaclem2  20153  dvdsrmul  20442  dvdsr01  20449  irredrmul  20505  rhmdvdsr  20605  rgspnval  20711  rgspncl  20712  lspf  21095  lspval  21096  lssats2  21121  lspfixed  21252  lspsolvlem  21266  zringlpir  21617  pzriprnglem13  21643  zncyg  21698  cygth  21721  frlmup4  21951  aspval  22022  evlseu  22234  fiinbas  23109  topbas  23129  pptbas  23165  clsval  23194  elcls  23230  neiint  23261  neips  23270  opnneissb  23271  opnssneib  23272  innei  23282  neiptopnei  23289  restbas  23315  neitr  23337  pnfnei  23377  mnfnei  23378  lmconst  23418  iscnp4  23420  cncnpi  23435  cnconst2  23440  cnprest  23446  cnpdis  23450  nrmsep  23514  regsep2  23533  cmpcovf  23548  cmpsub  23557  cmpcld  23559  hauscmplem  23563  conncompid  23588  2ndci  23605  2ndcsb  23606  2ndc1stc  23608  1stcrest  23610  2ndcctbss  23612  2ndcdisj  23613  2ndcomap  23615  2ndcsep  23616  dis2ndc  23617  restlly  23640  islly2  23641  hausllycmp  23651  cldllycmp  23652  lly1stc  23653  dislly  23654  ssref  23669  refref  23670  finlocfin  23677  dissnlocfin  23686  locfindis  23687  llycmpkgen2  23707  cmpkgen  23708  1stckgenlem  23710  elptr  23730  ptbasfi  23738  neitx  23764  ptpjopn  23769  txcnp  23777  ptcnplem  23778  txlly  23793  txnlly  23794  txtube  23797  txcmplem1  23798  tx1stc  23807  txkgen  23809  xkococnlem  23816  txconn  23846  tgqtop  23869  kqreglem1  23898  kqreglem2  23899  kqnrmlem1  23900  kqnrmlem2  23901  reghmph  23950  nrmhmph  23951  fbssfi  23994  opnfbas  23999  isfil2  24013  fsubbas  24024  ssfg  24029  fgss2  24031  fbasrn  24041  filuni  24042  fgtr  24047  ssufl  24075  uffix  24078  elfm2  24105  elfm3  24107  imaelfm  24108  rnelfmlem  24109  rnelfm  24110  fmfnfmlem4  24114  fmfnfm  24115  fmco  24118  ufldom  24119  hausflim  24138  flimcls  24142  hauspwpwf1  24144  flffbas  24152  txflf  24163  fclscf  24182  fclsfnflim  24184  alexsubALTlem4  24207  alexsubALT  24208  tmdgsum2  24253  symgtgp  24263  subgntr  24264  opnsubg  24265  ghmcnp  24272  qustgpopn  24277  tsmsfbas  24285  tsmsxplem1  24310  ustexsym  24373  trust  24386  utoptop  24391  restutop  24394  restutopopn  24395  ustuqtop4  24401  utopsnneiplem  24404  iducn  24439  fmucnd  24448  cfilufg  24449  trcfilu  24450  neipcfilu  24452  imasdsf1olem  24530  blssps  24581  blss  24582  blssexps  24583  blssex  24584  ssblex  24585  blin2  24586  neibl  24658  blcld  24662  metss2  24669  stdbdmopn  24675  met1stc  24678  met2ndci  24679  metrest  24681  prdsxmslem2  24686  metcnp3  24697  metustexhalf  24713  metustfbas  24714  cfilucfil  24716  restmetu  24727  dscopn  24730  ngptgp  24793  nlmvscnlem1  24843  tgioo  24953  tgqioo  24957  xrsmopn  24970  zcld  24971  recld2  24972  zdis  24974  icccmplem1  24980  icccmplem2  24981  xmetdcn2  24995  addcnlem  25022  xrhmeo  25105  cnheibor  25114  cnllycmp  25115  lebnumlem3  25122  lebnum  25123  xlebnum  25124  lebnumii  25125  elpi1i  25205  ipcnlem1  25404  lmnn  25422  iscfil3  25432  cfilres  25455  flimcfil  25473  bcthlem4  25486  bcthlem5  25487  minveclem4c  25584  minveclem2  25585  minveclem3b  25587  minveclem3  25588  minveclem4  25591  minveclem6  25593  ivthlem2  25611  ivth  25613  ivthle  25615  ivthle2  25616  elovolmr  25635  ovolunlem1  25656  ovoliunlem2  25662  ovolicc1  25675  iundisj  25707  iunmbl2  25716  dyadmbllem  25758  volivth  25766  mbflimsup  25825  i1faddlem  25852  i1fmullem  25853  itg2lr  25889  itg2monolem1  25909  limcnlp  26037  ellimc3  26038  limcflf  26040  limciun  26053  rollelem  26148  c1lip1  26156  lhop1lem  26172  ply1divex  26294  ig1peu  26332  elply2  26353  coeeq  26384  plydivlem3  26456  plydivlem4  26457  elqaalem3  26482  qaa  26484  iaa  26488  aareccl  26489  aannenlem2  26492  aalioulem2  26496  aalioulem3  26497  aalioulem5  26499  aalioulem6  26500  aaliou  26501  aaliou2  26503  aaliou3lem8  26508  ulmshftlem  26552  reeff1o  26610  pilem2  26615  pilem3  26616  efif1olem2  26708  efopn  26823  cxpcn3lem  26912  cxpeq  26922  dcubic2  27009  quart  27026  xrlimcnp  27133  ftalem5  27241  ftalem7  27243  sgmnncl  27311  dvdsppwf1o  27350  musum  27355  perfect  27395  dchrptlem1  27428  dchrptlem2  27429  dchrpt  27431  bpos1lem  27446  lgsqrlem4  27513  lgsdchrval  27518  2sqblem  27595  dchrisumlem3  27655  chpdifbndlem2  27718  pntrsumbnd2  27731  pntpbnd1  27750  pntpbnd2  27751  pntpbnd  27752  pntibndlem2  27755  pntibndlem3  27756  pntleme  27772  pntlem3  27773  elno2  27818  ltsval2  27820  noreson  27824  ltsres  27826  noseponlem  27828  nolesgn2o  27835  nogesgn1o  27837  nodense  27856  nosupfv  27870  nosupres  27871  nosupbnd1lem3  27874  nosupbnd1lem5  27876  nosupbnd2lem1  27879  noinffv  27885  noinfres  27886  noinfbnd1lem3  27889  noinfbnd1lem5  27891  noinfbnd2lem1  27894  noetasuplem4  27900  noetainflem4  27904  noetalem2  27906  cuteq0  28008  cuteq1  28010  oldlim  28080  bdayiun  28108  cofcutrtime  28120  cofss  28123  coiniss  28124  cutlt  28125  cutmax  28127  cutmin  28128  negsex  28236  negsfo  28246  norecdiv  28383  divs1  28397  precsexlem11  28410  precsex  28411  recsex  28412  elons2d  28452  oncutlt  28457  n0on  28529  bdayn0sf1o  28563  dfnns2  28565  zsoring  28602  pw2recs  28631  halfcut  28651  0reno  28689  1reno  28690  readdscl  28692  axtgcont  28738  tgcgrxfr  28787  legid  28856  btwnleg  28857  leg0  28861  tghilberti1  28910  colline  28923  mirreu3  28931  isperp2  28995  colperpex  29014  lnopp2hpgb  29045  hpgerlem  29047  brbtwn  29249  brcgr  29250  brbtwn2  29255  axpasch  29291  axlowdimlem14  29305  axlowdim2  29310  axcontlem2  29315  axcontlem4  29317  axcontlem8  29321  axcontlem10  29323  axcontlem12  29325  fusgrn0degnn0  29849  friendshipgt3  30749  lpni  30832  isgrpoi  30850  vacn  31046  smcnlem  31049  nmosetn0  31117  nmoolb  31123  nmobndi  31127  nmoo0  31143  nmlno0lem  31145  isblo3i  31153  blo3i  31154  blocnilem  31156  ubthlem1  31222  minvecolem2  31227  minvecolem3  31228  minvecolem4c  31231  minvecolem4  31232  minvecolem5  31233  minvecolem6  31234  norm1exi  31602  occl  31656  spanval  31685  spancl  31688  shsval2i  31739  ococin  31760  pjoml6i  31941  nmopsetn0  32217  nmfnsetn0  32230  nmoplb  32259  nmfnlb  32276  nmop0  32338  nmfn0  32339  nmlnop0iALT  32347  nmopun  32366  nmcexi  32378  lnconi  32385  lnopcnbd  32388  lnfncnbd  32409  riesz3i  32414  riesz1  32417  cnlnadjlem2  32420  cnlnadjlem8  32426  cnlnadjlem9  32427  adjbd1o  32437  branmfn  32457  opsqrlem1  32492  pjnmopi  32500  strlem1  32602  stri  32609  hstri  32617  cvcon3  32636  cvnbtwn  32638  superpos  32706  shatomici  32710  atcvat4i  32749  mdsymlem2  32756  cdj1i  32785  cdj3i  32793  rexunirn  32838  foresf1o  32850  iundisjf  32934  aciunf1lem  33007  fnpreimac  33015  fgreu  33016  fcnvgreu  33017  xrge0infss  33105  ssnnssfz  33132  iundisjfi  33141  indf1ofs  33186  xreceu  33241  rexdiv  33245  isarchi3  33507  archirngz  33509  archiabllem2a  33514  0nellinds  33685  qtophaus  34226  reff  34229  locfinreflem  34230  cmpcref  34240  dispcmp  34249  tpr2rico  34302  pnfneige0  34341  qqhucn  34382  rrhre  34411  esumcst  34453  esumpcvgval  34468  dmsigagen  34534  rossros  34570  dya2icoseg  34667  dya2iocnrect  34671  dya2iocuni  34673  eulerpartlemgvv  34766  dstfrvunirn  34865  ballotlem4  34889  ballotlemic  34897  ballotlemrc  34921  signsw0g  34943  signswmnd  34944  prodfzo03  34990  tgoldbachgt  35050  onvf1odlem4  35590  loop1cycl  35629  umgr2cycllem  35632  umgr2cycl  35633  subfacp1lem3  35674  erdsze2lem2  35696  cnpconn  35722  txpconn  35724  ptpconn  35725  indispconn  35726  connpconn  35727  cvxpconn  35734  cnllysconn  35737  cvmsss2  35766  cvmcov2  35767  cvmopnlem  35770  cvmliftlem14  35789  cvmliftlem15  35790  cvmlift2lem11  35805  cvmlift2lem12  35806  cvmlift2lem13  35807  cvmlift3lem2  35812  cvmlift3lem6  35816  cvmlift3lem9  35819  mthmi  36069  r1peuqusdeg1  36135  br8  36248  br6  36249  br4  36250  dfon2lem9  36281  wzel  36314  wsuclem  36315  wsuclb  36318  imagesset  36445  fvtransport  36524  brcolinear  36551  brsegle  36600  seglerflx  36604  seglemin  36605  btwnsegle  36609  fvray  36633  fvline  36636  hilbert1.1  36646  elhf2  36667  0hf  36669  nn0prpwlem  36853  nn0prpw  36854  fness  36880  fneref  36881  fnessref  36888  refssfne  36889  neibastop2lem  36891  fnemeet1  36897  tailfb  36908  filnetlem4  36912  limsucncmpi  36976  ttctr  37024  dfttc2g  37037  taupilemrplb  37984  qdiff  37991  relowlssretop  38029  rdgellim  38042  matunitlindflem2  38288  ptrecube  38291  poimirlem4  38295  poimirlem17  38308  poimirlem20  38311  poimirlem23  38314  poimirlem24  38315  poimirlem26  38317  poimirlem27  38318  poimirlem29  38320  poimirlem32  38323  heicant  38326  mblfinlem1  38328  mblfinlem2  38329  mblfinlem3  38330  mblfinlem4  38331  ismblfin  38332  volsupnfl  38336  itg2addnclem  38342  itg2addnclem3  38344  itg2addnc  38345  ftc1anclem5  38368  unirep  38385  cover2  38386  indexa  38404  frinfm  38406  sdclem1  38414  fdc  38416  incsequz  38419  caushft  38432  istotbnd3  38442  0totbnd  38444  sstotbnd2  38445  sstotbnd  38446  sstotbnd3  38447  isbnd3  38455  ssbnd  38459  equivbnd  38461  prdsbnd  38464  prdstotbnd  38465  cntotbnd  38467  heibor1lem  38480  heiborlem1  38482  heiborlem3  38484  heiborlem6  38487  heiborlem8  38489  bfplem2  38494  rrncmslem  38503  iccbnd  38511  opidonOLD  38523  exidres  38549  isrngod  38569  isgrpda  38626  isdrngo2  38629  igenval  38732  igenidl  38734  prtlem10  39659  lshpnel2N  39779  lsmsat  39802  lssatomic  39805  lcvnbtwn  39819  lfl1  39864  eqlkr  39893  lshpkrlem1  39904  lshpkrex  39912  cvrcon3b  40071  cvrat4  40237  3dim3  40263  ps-2  40272  llni  40302  llnle  40312  lplni  40326  lplnle  40334  lplnexllnN  40358  lvoli  40369  lnatexN  40573  elpaddn0  40594  pclfinN  40694  lhprelat3N  40834  4atexlemex2  40865  4atex  40870  4atex2-0aOLDN  40872  4atex2-0cOLDN  40874  lautcvr  40886  cdleme0ex1N  41017  cdleme50rnlem  41338  cdleme50ex  41353  cdlemg1cex  41382  cdlemkid5  41729  cdlemk  41768  tendoex  41769  cdleml5N  41774  cdlemm10N  41912  dih1dimatlem0  42122  dihjat1lem  42222  dvh3dim2  42242  dvh3dim3N  42243  dochkr1  42272  dochkr1OLDN  42273  lcfrvalsnN  42335  lcfrlem27  42363  lcfrlem37  42373  lcfr  42379  mapd1o  42442  mapdpglem23  42488  hdmap11lem2  42636  primrootsunit1  42884  zdivgd  43118  resubeu  43158  fidomncyc  43323  nacsfix  43463  mzpcompact2lem  43502  eldioph  43509  diophrw  43510  diophin  43523  rexrabdioph  43541  rexzrexnn0  43551  eldioph4b  43558  rencldnfilem  43567  irrapxlem5  43573  irrapxlem6  43574  pell1234qrdich  43608  pell14qrdich  43616  infmrgelbi  43625  pellqrex  43626  pellfundre  43628  pellfundlb  43631  rmxynorm  43665  congrep  43720  acongrep  43727  jm2.27  43755  fnwe2lem2  43798  islssfgi  43819  hbtlem2  43871  hbtlem4  43873  hbtlem5  43875  dgraaub  43895  mpaaeu  43897  aaitgo  43909  unielss  43965  onexgt  43987  onexomgt  43988  onexlimgt  43990  onexoegt  43991  oaordnr  44043  omnord1  44052  oenord1  44063  oaomoencom  44064  oenass  44066  tfsconcatfv2  44087  tfsconcatrn  44089  tfsconcatb0  44091  ofoafo  44103  naddcnffo  44111  oaun3lem1  44121  naddwordnexlem4  44148  sucomisnotcard  44290  clsk1independent  44792  0elaxnul  45712  pwclaxpow  45713  prclaxpr  45714  uniclaxun  45715  omssaxinf2  45717  wfac8prim  45731  restuni3  45856  iinssd  45869  founiiun  45917  wessf1ornlem  45923  founiiun0  45928  unirnmap  45944  dstregt0  46021  uzfissfz  46062  rpgtrecnn  46115  rexabslelem  46152  infrnmptle  46157  infxrunb3rnmpt  46162  infxrpnf  46180  supminfxr  46198  rexanuz2nf  46226  iooiinicc  46278  iooiinioc  46292  uzubioo  46301  climsuse  46344  islptre  46355  limsuppnfdlem  46435  climinf3  46450  limsupmnfuzlem  46460  limsupre3lem  46466  limsupre3uzlem  46469  0cnv  46476  liminfreuzlem  46536  cnrefiisplem  46563  icccncfext  46621  cncficcgt0  46622  dvbdfbdioo  46664  ioodvbdlimc1lem1  46665  ioodvbdlimc1lem2  46666  ioodvbdlimc2lem  46668  stoweidlem9  46743  stoweidlem14  46748  stoweidlem18  46752  stoweidlem21  46755  stoweidlem29  46763  stoweidlem34  46768  stoweidlem35  46769  stoweidlem39  46773  stoweidlem41  46775  stoweidlem45  46779  stoweidlem52  46786  stoweidlem55  46789  stoweidlem57  46791  stoweidlem60  46794  stirlinglem5  46812  stirlinglem13  46820  stirlinglem14  46821  fourierdlem16  46857  fourierdlem20  46861  fourierdlem21  46862  fourierdlem22  46863  fourierdlem25  46866  fourierdlem31  46872  fourierdlem39  46880  fourierdlem41  46882  fourierdlem42  46883  fourierdlem47  46887  fourierdlem48  46888  fourierdlem51  46891  fourierdlem63  46903  fourierdlem64  46904  fourierdlem65  46905  fourierdlem77  46917  fourierdlem81  46921  fourierdlem83  46923  fourierdlem103  46943  fourierdlem104  46944  elaa2lem  46967  etransclem47  47015  qndenserrnbl  47029  ioorrnopnlem  47038  ioorrnopnxrlem  47040  intsaluni  47063  salgencntex  47077  subsaliuncllem  47091  sge0resplit  47140  sge0seq  47180  sge0reuz  47181  nnfoctbdjlem  47189  meaiininclem  47220  hoicvrrex  47290  ovnlecvr  47292  ovnlerp  47296  hoidmv1lelem2  47326  hoidmvlelem2  47330  hoidmvlelem3  47331  ovnhoilem1  47335  ovnlecvr2  47344  hoiqssbl  47359  ovolval4lem2  47384  ovolval5lem2  47387  ovnovollem1  47390  ovnovollem2  47391  iinhoiicclem  47407  smfinflem  47551  smflimsuplem7  47560  sqrtnnaa  47624  sprsymrelfolem2  48262  perfectALTV  48508  9gbo  48559  11gbo  48560  nnsum3primes4  48573  nnsum3primesprm  48575  ssnn0ssfz  49149  lincsumcl  49231  lincscmcl  49232  zlmodzxzldep  49304  ldepsnlinc  49308  line2ylem  49551  line2xlem  49553  sepfsepc  49726  lubsscl  49758  glbsscl  49759  nelsubc3lem  49868  cnelsubclem  50401  aacllem  50641