Theorem rspcev 3583

Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2179, ax-11 2195, ax-12 2216. (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 487	. . 3 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓))
4	1, 3	rspcedv 3576	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝜓 → ∃𝑥 ∈ 𝐵 𝜑))
5	4	imp 412	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ∃wrex 3091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092

This theorem is used by:  rspcedvdw  3586  rspceaimv  3589  rspc2ev  3596  rspc3ev  3600  rspceeqv  3606  reu6i  3693  rspesbca  3835  eliuni  4964  iuneqconst  4970  brralrspcev  5173  wefrc  5657  wereu2  5660  xpdifid  6167  xpdifcnvepel  6168  frpomin  6345  onfr  6404  onelssex  6414  ordunidif  6415  eliman0  6922  dffv2  6980  elrnrexdm  7088  eldmrexrn  7090  elabrex  7245  elabrexg  7246  f1elima  7266  fliftfun  7319  fliftval  7323  f1oiso2  7359  sorpssuni  7739  sorpssint  7740  onssmin  7797  onminex  7807  fimaproj  8137  frxp3  8153  poseq  8160  tfrlem12  8382  seqomlem2  8444  oawordeulem  8545  oaass  8552  odi  8570  omass  8571  omeulem1  8573  oen0  8578  oelim2  8587  oeeulem  8593  nnawordex  8629  nnaordex2  8631  eldifsucnn  8656  cofon1  8664  cofon2  8665  naddcllem  8668  naddunif  8686  boxcutc  8945  0fi  9046  snfi  9047  rexdif1en  9152  findcard  9155  nnfi  9159  pssnn  9160  unfi  9162  onfin  9206  dif1ennnALT  9244  frfi  9252  fisupg  9255  nnsdomg  9266  pwfir  9283  prfi  9290  fissuni  9321  fipreima  9322  finsschain  9323  indexfi  9324  marypha1lem  9400  eqsup  9423  supmax  9435  fisup2g  9436  fisupcl  9437  supisoex  9442  infmin  9463  fiinfg  9468  fiinf2g  9469  wofib  9514  wemaplem2  9516  card2inf  9524  brwdom2  9542  cnfcom3clem  9681  ssttrcl  9691  ttrcltr  9692  trcl  9704  frmin  9728  r1ordg  9757  r1pwss  9763  tz9.12lem3  9768  tz9.12  9769  r1elwf  9775  tcrank  9863  scottex  9869  scottexOLD  9870  scott0b  9873  scott0OLD  9874  isnumi  9948  onsdom  9998  ondomen  10037  infpwfien  10062  cardaleph  10089  infenaleph  10091  alephfplem4  10107  alephfp2  10109  dfac2b  10130  ackbij1lem18  10235  ackbij1  10236  cflem  10244  cflecard  10251  cfsuc  10256  cfflb  10258  cofsmo  10268  coftr  10272  fin23lem7  10315  fin23lem11  10316  enfin2i  10320  fin23lem26  10324  isf32lem5  10356  isf34lem4  10376  isfin1-3  10385  fin1a2lem7  10405  axdc3lem4  10452  ttukeylem7  10514  iunfo  10540  ficard  10566  pwcfsdom  10585  fpwwe2lem11  10643  wunex  10741  eltsk2g  10753  grur1  10822  axgroth6  10830  inaprc  10838  nqereu  10931  archnq  10982  genpnmax  11009  ltexpri  11045  prlem936  11049  recexpr  11053  supexpr  11056  negexsr  11104  recexsrlem  11105  recexsr  11109  supsrlem  11113  axrnegex  11164  axrrecex  11165  axpre-sup  11171  1re  11225  dedekind  11390  dedekindle  11391  cnegex  11408  cnegex2  11409  recex  11863  receu  11876  fiminre2  12180  cju  12231  nn2ge  12280  nominpos  12498  zdiv  12684  btwnz  12717  uzwo  12953  ublbneg  12975  lbzbi  12978  zsupss  12979  uzsupss  12982  rpnnen1lem1  13020  rpnnen1lem3  13021  rpnnen1lem4  13022  rpnnen1lem5  13023  z2ge  13242  qbtwnre  13243  qbtwnxr  13244  xralrple  13249  xrsupsslem  13351  xrinfmsslem  13352  supxrpnf  13362  icc0  13438  uzsup  13916  expnbnd  14288  expmulnbnd  14291  hashkf  14388  hashdom  14435  iswrdi  14574  rtrclreclem1  15120  rtrclreclem2  15122  rtrclreclem3  15123  01sqrex  15326  resqrex  15327  sqrtneg  15344  abs1m  15413  rexanuz  15423  rexuz3  15426  rexuzre  15430  sqreu  15438  o1lo1  15614  climconst  15620  rlimclim1  15622  climshftlem  15651  rlimo1  15694  lo1add  15704  lo1mul  15705  lo1le  15729  isercoll  15745  serf0  15758  zsum  15794  fsum  15796  fsumcvg3  15805  mertenslem1  15963  ntrivcvgn0  15977  ntrivcvgmullem  15980  zprod  16016  fprod  16020  fprodntriv  16021  dvdsval2  16337  dvds0lem  16348  dvds1lem  16349  dvds2lem  16350  odd2np1lem  16422  odd2np1  16423  opeo  16447  omeo  16448  divalglem9  16483  gcdcllem3  16583  lcmcllem  16678  qredeu  16740  exprmfct  16787  isprm5  16790  odzcllem  16876  reumodprminv  16888  modprm0  16889  nnnn0modprm0  16890  pythagtriplem19  16917  pcprmpw2  16966  pockthi  16991  infpnlem2  16995  vdwlem2  17066  vdwlem10  17074  vdwlem13  17077  ramub1lem1  17110  cshwrepswhash1  17186  imasleval  17619  mreexexlem3d  17726  mreexexlem4d  17727  iscatd  17753  cat1  18178  poslubd  18491  fpwipodrs  18620  ismgmid2  18754  mgmidsssn0  18758  mgmidpfod  18762  gsumval2a  18777  ismndd  18849  isgrpd2  19069  isgrpd  19071  imasgrp2  19167  mhmmnd  19176  ghmgrp  19178  gaorber  19424  orbsta  19429  cayleyth  19531  pmtrdifel  19596  pmtrdifwrdel  19601  pmtrdifwrdel2  19602  psgnunilem2  19611  psgnunilem3  19612  psgnvalii  19625  pgpfi1  19711  sylow1lem3  19716  sylow1lem5  19718  pgpfi  19721  sylow2alem2  19734  efgredeu  19868  lt6abl  20011  pgpfac1lem3a  20194  pgpfac1lem3  20195  pgpfac1lem5  20197  pgpfaclem1  20199  pgpfaclem3  20201  ablfaclem2  20204  dvdsrmul  20494  dvdsr01  20501  irredrmul  20557  rhmdvdsr  20657  rgspnval  20763  rgspncl  20764  lspf  21147  lspval  21148  lssats2  21173  lspfixed  21304  lspsolvlem  21318  zringlpir  21669  pzriprnglem13  21695  zncyg  21750  cygth  21773  frlmup4  22003  aspval  22074  evlseu  22286  fiinbas  23161  topbas  23181  pptbas  23217  clsval  23246  elcls  23282  neiint  23313  neips  23322  opnneissb  23323  opnssneib  23324  innei  23334  neiptopnei  23341  restbas  23367  neitr  23389  pnfnei  23429  mnfnei  23430  lmconst  23470  iscnp4  23472  cncnpi  23487  cnconst2  23492  cnprest  23498  cnpdis  23502  nrmsep  23566  regsep2  23585  cmpcovf  23600  cmpsub  23609  cmpcld  23611  hauscmplem  23615  conncompid  23640  2ndci  23657  2ndcsb  23658  2ndc1stc  23660  1stcrest  23662  2ndcctbss  23665  2ndcdisj  23666  2ndcomap  23668  2ndcsep  23669  dis2ndc  23670  restlly  23693  islly2  23694  hausllycmp  23704  cldllycmp  23705  lly1stc  23706  dislly  23707  ssref  23722  refref  23723  finlocfin  23730  dissnlocfin  23739  locfindis  23740  llycmpkgen2  23760  cmpkgen  23761  1stckgenlem  23763  elptr  23783  ptbasfi  23791  neitx  23817  ptpjopn  23822  txcnp  23830  ptcnplem  23831  txlly  23846  txnlly  23847  txtube  23850  txcmplem1  23851  tx1stc  23860  txkgen  23862  xkococnlem  23869  txconn  23899  tgqtop  23922  kqreglem1  23951  kqreglem2  23952  kqnrmlem1  23953  kqnrmlem2  23954  reghmph  24003  nrmhmph  24004  fbssfi  24047  opnfbas  24052  isfil2  24066  fsubbas  24077  ssfg  24082  fgss2  24084  fbasrn  24094  filuni  24095  fgtr  24100  ssufl  24128  uffix  24131  elfm2  24158  elfm3  24160  imaelfm  24161  rnelfmlem  24162  rnelfm  24163  fmfnfmlem4  24167  fmfnfm  24168  fmco  24171  ufldom  24172  hausflim  24191  flimcls  24195  hauspwpwf1  24197  flffbas  24205  txflf  24216  fclscf  24235  fclsfnflim  24237  alexsubALTlem4  24260  alexsubALT  24261  tmdgsum2  24306  symgtgp  24316  subgntr  24317  opnsubg  24318  ghmcnp  24325  qustgpopn  24330  tsmsfbas  24338  tsmsxplem1  24363  ustexsym  24426  trust  24439  utoptop  24444  restutop  24447  restutopopn  24448  ustuqtop4  24454  utopsnneiplem  24457  iducn  24492  fmucnd  24501  cfilufg  24502  trcfilu  24503  neipcfilu  24505  imasdsf1olem  24583  blssps  24634  blss  24635  blssexps  24636  blssex  24637  ssblex  24638  blin2  24639  neibl  24711  blcld  24715  metss2  24722  stdbdmopn  24728  met1stc  24731  met2ndci  24732  metrest  24734  prdsxmslem2  24739  metcnp3  24750  metustexhalf  24766  metustfbas  24767  cfilucfil  24769  restmetu  24780  dscopn  24783  ngptgp  24846  nlmvscnlem1  24896  tgioo  25006  tgqioo  25010  xrsmopn  25023  zcld  25024  recld2  25025  zdis  25027  icccmplem1  25033  icccmplem2  25034  xmetdcn2  25048  addcnlem  25075  xrhmeo  25158  cnheibor  25167  cnllycmp  25168  lebnumlem3  25175  lebnum  25176  xlebnum  25177  lebnumii  25178  elpi1i  25258  ipcnlem1  25457  lmnn  25475  iscfil3  25485  cfilres  25508  flimcfil  25526  bcthlem4  25539  bcthlem5  25540  minveclem4c  25637  minveclem2  25638  minveclem3b  25640  minveclem3  25641  minveclem4  25644  minveclem6  25646  ivthlem2  25664  ivth  25666  ivthle  25668  ivthle2  25669  elovolmr  25688  ovolunlem1  25709  ovoliunlem2  25715  ovolicc1  25728  iundisj  25760  iunmbl2  25769  dyadmbllem  25811  volivth  25819  mbflimsup  25878  i1faddlem  25905  i1fmullem  25906  itg2lr  25942  itg2monolem1  25962  limcnlp  26090  ellimc3  26091  limcflf  26093  limciun  26106  rollelem  26201  c1lip1  26209  lhop1lem  26225  ply1divex  26347  ig1peu  26385  elply2  26406  coeeq  26437  plydivlem3  26509  plydivlem4  26510  elqaalem3  26535  qaa  26537  iaa  26541  aareccl  26542  aannenlem2  26545  aalioulem2  26549  aalioulem3  26550  aalioulem5  26552  aalioulem6  26553  aaliou  26554  aaliou2  26556  aaliou3lem8  26561  ulmshftlem  26605  reeff1o  26663  pilem2  26668  pilem3  26669  efif1olem2  26761  efopn  26876  cxpcn3lem  26965  cxpeq  26975  dcubic2  27062  quart  27079  xrlimcnp  27186  ftalem5  27294  ftalem7  27296  sgmnncl  27364  dvdsppwf1o  27403  musum  27408  perfect  27448  dchrptlem1  27481  dchrptlem2  27482  dchrpt  27484  bpos1lem  27499  lgsqrlem4  27566  lgsdchrval  27571  2sqblem  27648  dchrisumlem3  27708  chpdifbndlem2  27771  pntrsumbnd2  27784  pntpbnd1  27803  pntpbnd2  27804  pntpbnd  27805  pntibndlem2  27808  pntibndlem3  27809  pntleme  27825  pntlem3  27826  elno2  27871  ltsval2  27873  noreson  27877  ltsres  27879  noseponlem  27881  nolesgn2o  27888  nogesgn1o  27890  nodense  27909  nosupfv  27923  nosupres  27924  nosupbnd1lem3  27927  nosupbnd1lem5  27929  nosupbnd2lem1  27932  noinffv  27938  noinfres  27939  noinfbnd1lem3  27942  noinfbnd1lem5  27944  noinfbnd2lem1  27947  noetasuplem4  27953  noetainflem4  27957  noetalem2  27959  cuteq0  28061  cuteq1  28063  oldlim  28133  bdayiun  28161  cofcutrtime  28173  cofss  28176  coiniss  28177  cutlt  28178  cutmax  28180  cutmin  28181  negsex  28289  negsfo  28299  norecdiv  28436  divs1  28450  precsexlem11  28463  precsex  28464  recsex  28465  elons2d  28505  oncutlt  28510  n0on  28582  bdayn0sf1o  28616  dfnns2  28618  zsoring  28655  pw2recs  28684  halfcut  28704  0reno  28742  1reno  28743  readdscl  28745  axtgcont  28791  tgcgrxfr  28840  legid  28909  btwnleg  28910  leg0  28914  tghilberti1  28963  colline  28976  mirreu3  28984  isperp2  29048  colperpex  29067  lnopp2hpgb  29098  hpgerlem  29100  brbtwn  29306  brcgr  29307  brbtwn2  29312  axpasch  29348  axlowdimlem14  29362  axlowdim2  29367  axcontlem2  29372  axcontlem4  29374  axcontlem8  29378  axcontlem10  29380  axcontlem12  29382  fusgrn0degnn0  29909  loop1cycl  30573  umgr2cycllem  30575  umgr2cycl  30576  friendshipgt3  30822  lpni  30905  isgrpoi  30923  vacn  31119  smcnlem  31122  nmosetn0  31190  nmoolb  31196  nmobndi  31200  nmoo0  31216  nmlno0lem  31218  isblo3i  31226  blo3i  31227  blocnilem  31229  ubthlem1  31295  minvecolem2  31300  minvecolem3  31301  minvecolem4c  31304  minvecolem4  31305  minvecolem5  31306  minvecolem6  31307  norm1exi  31675  occl  31729  spanval  31758  spancl  31761  shsval2i  31812  ococin  31833  pjoml6i  32014  nmopsetn0  32290  nmfnsetn0  32303  nmoplb  32332  nmfnlb  32349  nmop0  32411  nmfn0  32412  nmlnop0iALT  32420  nmopun  32439  nmcexi  32451  lnconi  32458  lnopcnbd  32461  lnfncnbd  32482  riesz3i  32487  riesz1  32490  cnlnadjlem2  32493  cnlnadjlem8  32499  cnlnadjlem9  32500  adjbd1o  32510  branmfn  32530  opsqrlem1  32565  pjnmopi  32573  strlem1  32675  stri  32682  hstri  32690  cvcon3  32709  cvnbtwn  32711  superpos  32779  shatomici  32783  atcvat4i  32822  mdsymlem2  32829  cdj1i  32858  cdj3i  32866  rexunirn  32911  foresf1o  32923  iundisjf  33007  aciunf1lem  33080  fnpreimac  33088  fgreu  33089  fcnvgreu  33090  xrge0infss  33177  ssnnssfz  33204  iundisjfi  33213  indf1ofs  33258  xreceu  33313  rexdiv  33317  isarchi3  33573  archirngz  33575  archiabllem2a  33580  0nellinds  33751  qtophaus  34292  reff  34295  locfinreflem  34296  cmpcref  34306  dispcmp  34315  tpr2rico  34368  pnfneige0  34407  qqhucn  34448  rrhre  34477  esumcst  34519  esumpcvgval  34534  dmsigagen  34601  rossros  34637  dya2icoseg  34734  dya2iocnrect  34738  dya2iocuni  34740  eulerpartlemgvv  34833  dstfrvunirn  34932  ballotlem4  34956  ballotlemic  34964  ballotlemrc  34988  signsw0g  35010  signswmnd  35011  prodfzo03  35057  tgoldbachgt  35117  onvf1odlem4  35649  subfacp1lem3  35713  erdsze2lem2  35735  cnpconn  35761  txpconn  35763  ptpconn  35764  indispconn  35765  connpconn  35766  cvxpconn  35773  cnllysconn  35776  cvmsss2  35805  cvmcov2  35806  cvmopnlem  35809  cvmliftlem14  35828  cvmliftlem15  35829  cvmlift2lem11  35844  cvmlift2lem12  35845  cvmlift2lem13  35846  cvmlift3lem2  35851  cvmlift3lem6  35855  cvmlift3lem9  35858  mthmi  36108  r1peuqusdeg1  36174  br8  36287  br6  36288  br4  36289  dfon2lem9  36320  wzel  36353  wsuclem  36354  wsuclb  36357  imagesset  36484  fvtransport  36563  brcolinear  36590  brsegle  36639  seglerflx  36643  seglemin  36644  btwnsegle  36648  fvray  36672  fvline  36675  hilbert1.1  36685  elhf2  36706  0hf  36708  nn0prpwlem  36892  nn0prpw  36893  fness  36919  fneref  36920  fnessref  36927  refssfne  36928  neibastop2lem  36930  fnemeet1  36936  tailfb  36947  filnetlem4  36951  limsucncmpi  37015  ttctr  37063  dfttc2g  37076  taupilemrplb  38023  qdiff  38030  relowlssretop  38068  rdgellim  38081  matunitlindflem2  38327  ptrecube  38330  poimirlem4  38334  poimirlem17  38347  poimirlem20  38350  poimirlem23  38353  poimirlem24  38354  poimirlem26  38356  poimirlem27  38357  poimirlem29  38359  poimirlem32  38362  heicant  38365  mblfinlem1  38367  mblfinlem2  38368  mblfinlem3  38369  mblfinlem4  38370  ismblfin  38371  volsupnfl  38375  itg2addnclem  38381  itg2addnclem3  38383  itg2addnc  38384  ftc1anclem5  38407  unirep  38425  cover2  38426  indexa  38444  frinfm  38446  sdclem1  38454  fdc  38456  incsequz  38459  caushft  38472  istotbnd3  38482  0totbnd  38484  sstotbnd2  38485  sstotbnd  38486  sstotbnd3  38487  isbnd3  38495  ssbnd  38499  equivbnd  38501  prdsbnd  38504  prdstotbnd  38505  cntotbnd  38507  heibor1lem  38520  heiborlem1  38522  heiborlem3  38524  heiborlem6  38527  heiborlem8  38529  bfplem2  38534  rrncmslem  38543  iccbnd  38551  opidonOLD  38563  exidres  38589  isrngod  38609  isgrpda  38666  isdrngo2  38669  igenval  38772  igenidl  38774  prtlem10  39699  lshpnel2N  39819  lsmsat  39842  lssatomic  39845  lcvnbtwn  39859  lfl1  39904  eqlkr  39933  lshpkrlem1  39944  lshpkrex  39952  cvrcon3b  40111  cvrat4  40277  3dim3  40303  ps-2  40312  llni  40342  llnle  40352  lplni  40366  lplnle  40374  lplnexllnN  40398  lvoli  40409  lnatexN  40613  elpaddn0  40634  pclfinN  40734  lhprelat3N  40874  4atexlemex2  40905  4atex  40910  4atex2-0aOLDN  40912  4atex2-0cOLDN  40914  lautcvr  40926  cdleme0ex1N  41057  cdleme50rnlem  41378  cdleme50ex  41393  cdlemg1cex  41422  cdlemkid5  41769  cdlemk  41808  tendoex  41809  cdleml5N  41814  cdlemm10N  41952  dih1dimatlem0  42162  dihjat1lem  42262  dvh3dim2  42282  dvh3dim3N  42283  dochkr1  42312  dochkr1OLDN  42313  lcfrvalsnN  42375  lcfrlem27  42403  lcfrlem37  42413  lcfr  42419  mapd1o  42482  mapdpglem23  42528  hdmap11lem2  42676  primrootsunit1  42924  zdivgd  43158  resubeu  43198  fidomncyc  43363  nacsfix  43503  mzpcompact2lem  43542  eldioph  43549  diophrw  43550  diophin  43563  rexrabdioph  43581  rexzrexnn0  43591  eldioph4b  43598  rencldnfilem  43607  irrapxlem5  43613  irrapxlem6  43614  pell1234qrdich  43648  pell14qrdich  43656  infmrgelbi  43665  pellqrex  43666  pellfundre  43668  pellfundlb  43671  rmxynorm  43705  congrep  43760  acongrep  43767  jm2.27  43795  fnwe2lem2  43838  islssfgi  43859  hbtlem2  43911  hbtlem4  43913  hbtlem5  43915  dgraaub  43935  mpaaeu  43937  aaitgo  43949  unielss  44005  onexgt  44027  onexomgt  44028  onexlimgt  44030  onexoegt  44031  oaordnr  44083  omnord1  44092  oenord1  44103  oaomoencom  44104  oenass  44106  tfsconcatfv2  44127  tfsconcatrn  44129  tfsconcatb0  44131  ofoafo  44143  naddcnffo  44151  oaun3lem1  44161  naddwordnexlem4  44188  sucomisnotcard  44330  clsk1independent  44832  0elaxnul  45752  pwclaxpow  45753  prclaxpr  45754  uniclaxun  45755  omssaxinf2  45757  wfac8prim  45771  restuni3  45896  iinssd  45909  founiiun  45957  wessf1ornlem  45963  founiiun0  45968  unirnmap  45984  dstregt0  46061  uzfissfz  46102  rpgtrecnn  46155  rexabslelem  46192  infrnmptle  46197  infxrunb3rnmpt  46202  infxrpnf  46220  supminfxr  46238  rexanuz2nf  46266  iooiinicc  46318  iooiinioc  46332  uzubioo  46341  climsuse  46384  islptre  46395  limsuppnfdlem  46475  climinf3  46490  limsupmnfuzlem  46500  limsupre3lem  46506  limsupre3uzlem  46509  0cnv  46516  liminfreuzlem  46576  cnrefiisplem  46603  icccncfext  46661  cncficcgt0  46662  dvbdfbdioo  46704  ioodvbdlimc1lem1  46705  ioodvbdlimc1lem2  46706  ioodvbdlimc2lem  46708  stoweidlem9  46783  stoweidlem14  46788  stoweidlem18  46792  stoweidlem21  46795  stoweidlem29  46803  stoweidlem34  46808  stoweidlem35  46809  stoweidlem39  46813  stoweidlem41  46815  stoweidlem45  46819  stoweidlem52  46826  stoweidlem55  46829  stoweidlem57  46831  stoweidlem60  46834  stirlinglem5  46852  stirlinglem13  46860  stirlinglem14  46861  fourierdlem16  46897  fourierdlem20  46901  fourierdlem21  46902  fourierdlem22  46903  fourierdlem25  46906  fourierdlem31  46912  fourierdlem39  46920  fourierdlem41  46922  fourierdlem42  46923  fourierdlem47  46927  fourierdlem48  46928  fourierdlem51  46931  fourierdlem63  46943  fourierdlem64  46944  fourierdlem65  46945  fourierdlem77  46957  fourierdlem81  46961  fourierdlem83  46963  fourierdlem103  46983  fourierdlem104  46984  elaa2lem  47007  etransclem47  47055  qndenserrnbl  47069  ioorrnopnlem  47078  ioorrnopnxrlem  47080  intsaluni  47103  salgencntex  47117  subsaliuncllem  47131  sge0resplit  47180  sge0seq  47220  sge0reuz  47221  nnfoctbdjlem  47229  meaiininclem  47260  hoicvrrex  47330  ovnlecvr  47332  ovnlerp  47336  hoidmv1lelem2  47366  hoidmvlelem2  47370  hoidmvlelem3  47371  ovnhoilem1  47375  ovnlecvr2  47384  hoiqssbl  47399  ovolval4lem2  47424  ovolval5lem2  47427  ovnovollem1  47430  ovnovollem2  47431  iinhoiicclem  47447  smfinflem  47591  smflimsuplem7  47600  sqrtnnaa  47664  sprsymrelfolem2  48302  perfectALTV  48548  9gbo  48599  11gbo  48600  nnsum3primes4  48613  nnsum3primesprm  48615  ssnn0ssfz  49188  lincsumcl  49270  lincscmcl  49271  zlmodzxzldep  49343  ldepsnlinc  49347  line2ylem  49590  line2xlem  49592  sepfsepc  49765  lubsscl  49797  glbsscl  49798  nelsubc3lem  49907  cnelsubclem  50440  aacllem  50680