Theorem rspcev 3574

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

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

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059

This theorem is referenced by:  rspcedvdw  3577  rspceb2dv  3578  rspceaimv  3580  rspc2ev  3587  rspc3ev  3591  rspceeqv  3597  reu6i  3684  rspesbca  3829  eliuni  4950  iuneqconst  4956  brralrspcev  5156  wefrc  5616  wereu2  5619  xpdifid  6124  frpomin  6296  onfr  6354  onelssex  6364  ordunidif  6365  eliman0  6869  dffv2  6927  elrnrexdm  7032  eldmrexrn  7034  elabrex  7186  elabrexg  7187  f1elima  7207  fliftfun  7256  fliftval  7260  f1oiso2  7296  sorpssuni  7675  sorpssint  7676  onssmin  7735  onminex  7745  fimaproj  8075  frxp3  8091  poseq  8098  tfrlem12  8318  seqomlem2  8380  oawordeulem  8479  oaass  8486  odi  8504  omass  8505  omeulem1  8507  oen0  8512  oelim2  8521  oeeulem  8527  nnawordex  8563  nnaordex2  8565  eldifsucnn  8590  cofon1  8598  cofon2  8599  naddcllem  8602  naddunif  8619  boxcutc  8877  0fi  8977  snfi  8978  rexdif1en  9083  findcard  9086  nnfi  9090  pssnn  9091  unfi  9093  onfin  9137  dif1ennnALT  9175  frfi  9183  fisupg  9186  nnsdomg  9197  pwfir  9215  prfi  9222  fissuni  9255  fipreima  9256  finsschain  9257  indexfi  9258  marypha1lem  9334  eqsup  9357  supmax  9369  fisup2g  9370  fisupcl  9371  supisoex  9376  infmin  9397  fiinfg  9402  fiinf2g  9403  wofib  9448  wemaplem2  9450  card2inf  9458  brwdom2  9476  cnfcom3clem  9612  ssttrcl  9622  ttrcltr  9623  trcl  9635  frmin  9659  r1ordg  9688  r1pwss  9694  tz9.12lem3  9699  tz9.12  9700  r1elwf  9706  tcrank  9794  scottex  9795  scott0  9796  isnumi  9856  onsdom  9906  ondomen  9945  infpwfien  9970  cardaleph  9997  infenaleph  9999  alephfplem4  10015  alephfp2  10017  dfac2b  10039  ackbij1lem18  10144  ackbij1  10145  cflem  10153  cflemOLD  10154  cflecard  10161  cfsuc  10165  cfflb  10167  cofsmo  10177  coftr  10181  fin23lem7  10224  fin23lem11  10225  enfin2i  10229  fin23lem26  10233  isf32lem5  10265  isf34lem4  10285  isfin1-3  10294  fin1a2lem7  10314  axdc3lem4  10361  ttukeylem7  10423  iunfo  10447  ficard  10473  pwcfsdom  10492  fpwwe2lem11  10550  wunex  10648  eltsk2g  10660  grur1  10729  axgroth6  10737  inaprc  10745  nqereu  10838  archnq  10889  genpnmax  10916  ltexpri  10952  prlem936  10956  recexpr  10960  supexpr  10963  negexsr  11011  recexsrlem  11012  recexsr  11016  supsrlem  11020  axrnegex  11071  axrrecex  11072  axpre-sup  11078  1re  11130  dedekind  11294  dedekindle  11295  cnegex  11312  cnegex2  11313  recex  11767  receu  11780  fiminre2  12088  cju  12139  nn2ge  12170  nominpos  12376  zdiv  12560  btwnz  12593  uzwo  12822  ublbneg  12844  lbzbi  12847  zsupss  12848  uzsupss  12851  rpnnen1lem1  12889  rpnnen1lem3  12890  rpnnen1lem4  12891  rpnnen1lem5  12892  z2ge  13111  qbtwnre  13112  qbtwnxr  13113  xralrple  13118  xrsupsslem  13220  xrinfmsslem  13221  supxrpnf  13231  icc0  13307  uzsup  13781  expnbnd  14153  expmulnbnd  14156  hashkf  14253  hashdom  14300  iswrdi  14438  rtrclreclem1  14978  rtrclreclem2  14980  rtrclreclem3  14981  01sqrex  15170  resqrex  15171  sqrtneg  15188  abs1m  15257  rexanuz  15267  rexuz3  15270  rexuzre  15274  sqreu  15282  o1lo1  15458  climconst  15464  rlimclim1  15466  climshftlem  15495  rlimo1  15538  lo1add  15548  lo1mul  15549  lo1le  15573  isercoll  15589  serf0  15602  zsum  15639  fsum  15641  fsumcvg3  15650  mertenslem1  15805  ntrivcvgn0  15819  ntrivcvgmullem  15822  zprod  15858  fprod  15862  fprodntriv  15863  dvdsval2  16180  dvds0lem  16191  dvds1lem  16192  dvds2lem  16193  odd2np1lem  16265  odd2np1  16266  opeo  16290  omeo  16291  divalglem9  16326  gcdcllem3  16426  lcmcllem  16521  qredeu  16583  exprmfct  16629  isprm5  16632  odzcllem  16718  reumodprminv  16730  modprm0  16731  nnnn0modprm0  16732  pythagtriplem19  16759  pcprmpw2  16808  pockthi  16833  infpnlem2  16837  vdwlem2  16908  vdwlem10  16916  vdwlem13  16919  ramub1lem1  16952  cshwrepswhash1  17028  imasleval  17460  mreexexlem3d  17567  mreexexlem4d  17568  iscatd  17594  cat1  18019  poslubd  18332  fpwipodrs  18461  ismgmid2  18591  mgmidsssn0  18595  gsumval2a  18608  ismndd  18679  isgrpd2  18884  isgrpd  18886  imasgrp2  18983  mhmmnd  18992  ghmgrp  18994  gaorber  19235  orbsta  19240  cayleyth  19342  pmtrdifel  19407  pmtrdifwrdel  19412  pmtrdifwrdel2  19413  psgnunilem2  19422  psgnunilem3  19423  psgnvalii  19436  pgpfi1  19522  sylow1lem3  19527  sylow1lem5  19529  pgpfi  19532  sylow2alem2  19545  efgredeu  19679  lt6abl  19822  pgpfac1lem3a  20005  pgpfac1lem3  20006  pgpfac1lem5  20008  pgpfaclem1  20010  pgpfaclem3  20012  ablfaclem2  20015  dvdsrmul  20298  dvdsr01  20305  irredrmul  20361  rhmdvdsr  20439  rgspnval  20543  rgspncl  20544  lspf  20923  lspval  20924  lssats2  20949  lspfixed  21081  lspsolvlem  21095  zringlpir  21420  pzriprnglem13  21446  zncyg  21501  cygth  21524  frlmup4  21754  aspval  21826  evlseu  22036  fiinbas  22894  topbas  22914  pptbas  22950  clsval  22979  elcls  23015  neiint  23046  neips  23055  opnneissb  23056  opnssneib  23057  innei  23067  neiptopnei  23074  restbas  23100  neitr  23122  pnfnei  23162  mnfnei  23163  lmconst  23203  iscnp4  23205  cncnpi  23220  cnconst2  23225  cnprest  23231  cnpdis  23235  nrmsep  23299  regsep2  23318  cmpcovf  23333  cmpsub  23342  cmpcld  23344  hauscmplem  23348  conncompid  23373  2ndci  23390  2ndcsb  23391  2ndc1stc  23393  1stcrest  23395  2ndcctbss  23397  2ndcdisj  23398  2ndcomap  23400  2ndcsep  23401  dis2ndc  23402  restlly  23425  islly2  23426  hausllycmp  23436  cldllycmp  23437  lly1stc  23438  dislly  23439  ssref  23454  refref  23455  finlocfin  23462  dissnlocfin  23471  locfindis  23472  llycmpkgen2  23492  cmpkgen  23493  1stckgenlem  23495  elptr  23515  ptbasfi  23523  neitx  23549  ptpjopn  23554  txcnp  23562  ptcnplem  23563  txlly  23578  txnlly  23579  txtube  23582  txcmplem1  23583  tx1stc  23592  txkgen  23594  xkococnlem  23601  txconn  23631  tgqtop  23654  kqreglem1  23683  kqreglem2  23684  kqnrmlem1  23685  kqnrmlem2  23686  reghmph  23735  nrmhmph  23736  fbssfi  23779  opnfbas  23784  isfil2  23798  fsubbas  23809  ssfg  23814  fgss2  23816  fbasrn  23826  filuni  23827  fgtr  23832  ssufl  23860  uffix  23863  elfm2  23890  elfm3  23892  imaelfm  23893  rnelfmlem  23894  rnelfm  23895  fmfnfmlem4  23899  fmfnfm  23900  fmco  23903  ufldom  23904  hausflim  23923  flimcls  23927  hauspwpwf1  23929  flffbas  23937  txflf  23948  fclscf  23967  fclsfnflim  23969  alexsubALTlem4  23992  alexsubALT  23993  tmdgsum2  24038  symgtgp  24048  subgntr  24049  opnsubg  24050  ghmcnp  24057  qustgpopn  24062  tsmsfbas  24070  tsmsxplem1  24095  ustexsym  24158  trust  24171  utoptop  24176  restutop  24179  restutopopn  24180  ustuqtop4  24186  utopsnneiplem  24189  iducn  24224  fmucnd  24233  cfilufg  24234  trcfilu  24235  neipcfilu  24237  imasdsf1olem  24315  blssps  24366  blss  24367  blssexps  24368  blssex  24369  ssblex  24370  blin2  24371  neibl  24443  blcld  24447  metss2  24454  stdbdmopn  24460  met1stc  24463  met2ndci  24464  metrest  24466  prdsxmslem2  24471  metcnp3  24482  metustexhalf  24498  metustfbas  24499  cfilucfil  24501  restmetu  24512  dscopn  24515  ngptgp  24578  nlmvscnlem1  24628  tgioo  24738  tgqioo  24742  xrsmopn  24755  zcld  24756  recld2  24757  zdis  24759  icccmplem1  24765  icccmplem2  24766  xmetdcn2  24780  addcnlem  24807  xrhmeo  24898  cnheibor  24908  cnllycmp  24909  lebnumlem3  24916  lebnum  24917  xlebnum  24918  lebnumii  24919  elpi1i  25000  ipcnlem1  25199  lmnn  25217  iscfil3  25227  cfilres  25250  flimcfil  25268  bcthlem4  25281  bcthlem5  25282  minveclem4c  25379  minveclem2  25380  minveclem3b  25382  minveclem3  25383  minveclem4  25386  minveclem6  25388  ivthlem2  25407  ivth  25409  ivthle  25411  ivthle2  25412  elovolmr  25431  ovolunlem1  25452  ovoliunlem2  25458  ovolicc1  25471  iundisj  25503  iunmbl2  25512  dyadmbllem  25554  volivth  25562  mbflimsup  25621  i1faddlem  25648  i1fmullem  25649  itg2lr  25685  itg2monolem1  25705  limcnlp  25833  ellimc3  25834  limcflf  25836  limciun  25849  rollelem  25947  c1lip1  25956  lhop1lem  25972  ply1divex  26096  ig1peu  26134  elply2  26155  coeeq  26186  plydivlem3  26257  plydivlem4  26258  elqaalem3  26283  qaa  26285  iaa  26287  aareccl  26288  aannenlem2  26291  aalioulem2  26295  aalioulem3  26296  aalioulem5  26298  aalioulem6  26299  aaliou  26300  aaliou2  26302  aaliou3lem8  26307  ulmshftlem  26352  reeff1o  26411  pilem2  26416  pilem3  26417  efif1olem2  26506  efopn  26621  cxpcn3lem  26711  cxpeq  26721  dcubic2  26808  quart  26825  xrlimcnp  26932  ftalem5  27041  ftalem7  27043  sgmnncl  27111  dvdsppwf1o  27150  musum  27155  perfect  27196  dchrptlem1  27229  dchrptlem2  27230  dchrpt  27232  bpos1lem  27247  lgsqrlem4  27314  lgsdchrval  27319  2sqblem  27396  dchrisumlem3  27456  chpdifbndlem2  27519  pntrsumbnd2  27532  pntpbnd1  27551  pntpbnd2  27552  pntpbnd  27553  pntibndlem2  27556  pntibndlem3  27557  pntleme  27573  pntlem3  27574  elno2  27620  sltval2  27622  noreson  27626  sltres  27628  noseponlem  27630  nolesgn2o  27637  nogesgn1o  27639  nodense  27658  nosupfv  27672  nosupres  27673  nosupbnd1lem3  27676  nosupbnd1lem5  27678  nosupbnd2lem1  27681  noinffv  27687  noinfres  27688  noinfbnd1lem3  27691  noinfbnd1lem5  27693  noinfbnd2lem1  27696  noetasuplem4  27702  noetainflem4  27706  noetalem2  27708  cuteq0  27803  cuteq1  27805  oldlim  27859  bdayiun  27887  cofcutrtime  27898  cofss  27901  coiniss  27902  cutlt  27903  cutmax  27905  cutmin  27906  negsex  28012  negsfo  28022  norecdiv  28159  divs1  28173  precsexlem11  28185  precsex  28186  recsex  28187  elons2d  28227  onscutlt  28232  n0ons  28296  bdayn0sf1o  28328  dfnns2  28330  zsoring  28367  pw2recs  28396  halfcut  28415  0reno  28441  1reno  28442  readdscl  28444  axtgcont  28490  tgcgrxfr  28539  legid  28608  btwnleg  28609  leg0  28613  tghilberti1  28658  tglnpt2  28662  colline  28670  mirreu3  28675  isperp2  28736  colperpex  28754  lnopp2hpgb  28784  hpgerlem  28786  brbtwn  28921  brcgr  28922  brbtwn2  28927  axpasch  28963  axlowdimlem14  28977  axlowdim2  28982  axcontlem2  28987  axcontlem4  28989  axcontlem8  28993  axcontlem10  28995  axcontlem12  28997  fusgrn0degnn0  29522  friendshipgt3  30422  lpni  30504  isgrpoi  30522  vacn  30718  smcnlem  30721  nmosetn0  30789  nmoolb  30795  nmobndi  30799  nmoo0  30815  nmlno0lem  30817  isblo3i  30825  blo3i  30826  blocnilem  30828  ubthlem1  30894  minvecolem2  30899  minvecolem3  30900  minvecolem4c  30903  minvecolem4  30904  minvecolem5  30905  minvecolem6  30906  norm1exi  31274  occl  31328  spanval  31357  spancl  31360  shsval2i  31411  ococin  31432  pjoml6i  31613  nmopsetn0  31889  nmfnsetn0  31902  nmoplb  31931  nmfnlb  31948  nmop0  32010  nmfn0  32011  nmlnop0iALT  32019  nmopun  32038  nmcexi  32050  lnconi  32057  lnopcnbd  32060  lnfncnbd  32081  riesz3i  32086  riesz1  32089  cnlnadjlem2  32092  cnlnadjlem8  32098  cnlnadjlem9  32099  adjbd1o  32109  branmfn  32129  opsqrlem1  32164  pjnmopi  32172  strlem1  32274  stri  32281  hstri  32289  cvcon3  32308  cvnbtwn  32310  superpos  32378  shatomici  32382  atcvat4i  32421  mdsymlem2  32428  cdj1i  32457  cdj3i  32465  rexunirn  32515  foresf1o  32528  iundisjf  32613  aciunf1lem  32689  fnpreimac  32698  fgreu  32699  fcnvgreu  32700  xrge0infss  32789  ssnnssfz  32816  iundisjfi  32825  indf1ofs  32897  xreceu  32952  rexdiv  32956  isarchi3  33218  archirngz  33220  archiabllem2a  33225  0nellinds  33400  qtophaus  33942  reff  33945  locfinreflem  33946  cmpcref  33956  dispcmp  33965  tpr2rico  34018  pnfneige0  34057  qqhucn  34098  rrhre  34127  esumcst  34169  esumpcvgval  34184  dmsigagen  34250  rossros  34286  dya2icoseg  34383  dya2iocnrect  34387  dya2iocuni  34389  eulerpartlemgvv  34482  dstfrvunirn  34581  ballotlem4  34605  ballotlemic  34613  ballotlem1c  34614  ballotlemrc  34637  signsw0g  34662  signswmnd  34663  prodfzo03  34709  tgoldbachgt  34769  onvf1odlem4  35249  loop1cycl  35280  umgr2cycllem  35283  umgr2cycl  35284  subfacp1lem3  35325  erdsze2lem2  35347  cnpconn  35373  txpconn  35375  ptpconn  35376  indispconn  35377  connpconn  35378  cvxpconn  35385  cnllysconn  35388  cvmsss2  35417  cvmcov2  35418  cvmopnlem  35421  cvmliftlem14  35440  cvmliftlem15  35441  cvmlift2lem11  35456  cvmlift2lem12  35457  cvmlift2lem13  35458  cvmlift3lem2  35463  cvmlift3lem6  35467  cvmlift3lem9  35470  mthmi  35720  r1peuqusdeg1  35786  br8  35899  br6  35900  br4  35901  dfon2lem9  35932  wzel  35965  wsuclem  35966  wsuclb  35969  imagesset  36096  fvtransport  36175  brcolinear  36202  brsegle  36251  seglerflx  36255  seglemin  36256  btwnsegle  36260  fvray  36284  fvline  36287  hilbert1.1  36297  elhf2  36318  0hf  36320  nn0prpwlem  36465  nn0prpw  36466  fness  36492  fneref  36493  fnessref  36500  refssfne  36501  neibastop2lem  36503  fnemeet1  36509  tailfb  36520  filnetlem4  36524  limsucncmpi  36588  taupilemrplb  37464  relowlssretop  37507  rdgellim  37520  matunitlindflem2  37757  ptrecube  37760  poimirlem4  37764  poimirlem17  37777  poimirlem20  37780  poimirlem23  37783  poimirlem24  37784  poimirlem26  37786  poimirlem27  37787  poimirlem29  37789  poimirlem32  37792  heicant  37795  mblfinlem1  37797  mblfinlem2  37798  mblfinlem3  37799  mblfinlem4  37800  ismblfin  37801  volsupnfl  37805  itg2addnclem  37811  itg2addnclem3  37813  itg2addnc  37814  ftc1anclem5  37837  unirep  37854  cover2  37855  indexa  37873  frinfm  37875  sdclem1  37883  fdc  37885  incsequz  37888  caushft  37901  istotbnd3  37911  0totbnd  37913  sstotbnd2  37914  sstotbnd  37915  sstotbnd3  37916  isbnd3  37924  ssbnd  37928  equivbnd  37930  prdsbnd  37933  prdstotbnd  37934  cntotbnd  37936  heibor1lem  37949  heiborlem1  37951  heiborlem3  37953  heiborlem6  37956  heiborlem8  37958  bfplem2  37963  rrncmslem  37972  iccbnd  37980  opidonOLD  37992  exidres  38018  isrngod  38038  isgrpda  38095  isdrngo2  38098  igenval  38201  igenidl  38203  prtlem10  39064  lshpnel2N  39184  lsmsat  39207  lssatomic  39210  lcvnbtwn  39224  lfl1  39269  eqlkr  39298  lshpkrlem1  39309  lshpkrex  39317  cvrcon3b  39476  cvrat4  39642  3dim3  39668  ps-2  39677  llni  39707  llnle  39717  lplni  39731  lplnle  39739  lplnexllnN  39763  lvoli  39774  lnatexN  39978  elpaddn0  39999  pclfinN  40099  lhprelat3N  40239  4atexlemex2  40270  4atex  40275  4atex2-0aOLDN  40277  4atex2-0cOLDN  40279  lautcvr  40291  cdleme0ex1N  40422  cdleme50rnlem  40743  cdleme50ex  40758  cdlemg1cex  40787  cdlemkid5  41134  cdlemk  41173  tendoex  41174  cdleml5N  41179  cdlemm10N  41317  dih1dimatlem0  41527  dihjat1lem  41627  dvh3dim2  41647  dvh3dim3N  41648  dochkr1  41677  dochkr1OLDN  41678  lcfrvalsnN  41740  lcfrlem27  41768  lcfrlem37  41778  lcfr  41784  mapd1o  41847  mapdpglem23  41893  hdmap11lem2  42041  primrootsunit1  42290  zdivgd  42534  resubeu  42574  fidomncyc  42732  nacsfix  42896  mzpcompact2lem  42935  eldioph  42942  diophrw  42943  diophin  42956  rexrabdioph  42978  rexzrexnn0  42988  eldioph4b  42995  rencldnfilem  43004  irrapxlem5  43010  irrapxlem6  43011  pell1234qrdich  43045  pell14qrdich  43053  infmrgelbi  43062  pellqrex  43063  pellfundre  43065  pellfundlb  43068  rmxynorm  43102  congrep  43157  acongrep  43164  jm2.27  43192  fnwe2lem2  43235  islssfgi  43256  hbtlem2  43308  hbtlem4  43310  hbtlem5  43312  dgraaub  43332  mpaaeu  43334  aaitgo  43346  unielss  43402  onexgt  43424  onexomgt  43425  onexlimgt  43427  onexoegt  43428  oaordnr  43480  omnord1  43489  oenord1  43500  oaomoencom  43501  oenass  43503  tfsconcatfv2  43524  tfsconcatrn  43526  tfsconcatb0  43528  ofoafo  43540  naddcnffo  43548  oaun3lem1  43558  naddwordnexlem4  43585  sucomisnotcard  43727  clsk1independent  44229  0elaxnul  45166  pwclaxpow  45167  prclaxpr  45168  uniclaxun  45169  omssaxinf2  45171  wfac8prim  45185  restuni3  45304  iinssd  45317  founiiun  45365  wessf1ornlem  45371  founiiun0  45376  unirnmap  45394  dstregt0  45472  uzfissfz  45513  rpgtrecnn  45566  rexabslelem  45604  infrnmptle  45609  infxrunb3rnmpt  45614  infxrpnf  45632  supminfxr  45650  rexanuz2nf  45678  iooiinicc  45730  iooiinioc  45744  uzubioo  45753  climsuse  45796  islptre  45807  limsuppnfdlem  45887  climinf3  45902  limsupmnfuzlem  45912  limsupre3lem  45918  limsupre3uzlem  45921  0cnv  45928  liminfreuzlem  45988  cnrefiisplem  46015  icccncfext  46073  cncficcgt0  46074  dvbdfbdioo  46116  ioodvbdlimc1lem1  46117  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  stoweidlem9  46195  stoweidlem14  46200  stoweidlem18  46204  stoweidlem21  46207  stoweidlem29  46215  stoweidlem34  46220  stoweidlem35  46221  stoweidlem39  46225  stoweidlem41  46227  stoweidlem45  46231  stoweidlem52  46238  stoweidlem55  46241  stoweidlem57  46243  stoweidlem60  46246  stirlinglem5  46264  stirlinglem13  46272  stirlinglem14  46273  fourierdlem16  46309  fourierdlem20  46313  fourierdlem21  46314  fourierdlem22  46315  fourierdlem25  46318  fourierdlem31  46324  fourierdlem39  46332  fourierdlem41  46334  fourierdlem42  46335  fourierdlem47  46339  fourierdlem48  46340  fourierdlem49  46341  fourierdlem51  46343  fourierdlem63  46355  fourierdlem64  46356  fourierdlem65  46357  fourierdlem77  46369  fourierdlem81  46373  fourierdlem83  46375  fourierdlem103  46395  fourierdlem104  46396  elaa2lem  46419  etransclem47  46467  qndenserrnbl  46481  ioorrnopnlem  46490  ioorrnopnxrlem  46492  intsaluni  46515  salgencntex  46529  subsaliuncllem  46543  sge0resplit  46592  sge0seq  46632  sge0reuz  46633  nnfoctbdjlem  46641  meaiininclem  46672  hoicvrrex  46742  ovnlecvr  46744  ovnlerp  46748  hoidmv1lelem2  46778  hoidmvlelem2  46782  hoidmvlelem3  46783  ovnhoilem1  46787  ovnlecvr2  46796  hoiqssbl  46811  ovolval4lem2  46836  ovolval5lem2  46839  ovnovollem1  46842  ovnovollem2  46843  iinhoiicclem  46859  smfinflem  47003  smflimsuplem7  47012  nthrucw  47072  sprsymrelfolem2  47681  perfectALTV  47911  9gbo  47962  11gbo  47963  nnsum3primes4  47976  nnsum3primesprm  47978  ssnn0ssfz  48537  lincsumcl  48619  lincscmcl  48620  zlmodzxzldep  48692  ldepsnlinc  48696  line2ylem  48939  line2xlem  48941  sepfsepc  49115  lubsscl  49147  glbsscl  49148  nelsubc3lem  49257  cnelsubclem  49790  aacllem  49988