Theorem rspcev 3612

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∃wrex 3070

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071

This theorem is referenced by:  rspceaimv  3616  rspc2ev  3623  rspc3ev  3627  rspceeqv  3632  reu6i  3723  rspesbca  3874  eliuni  5002  iuneqconst  5007  brralrspcev  5207  wefrc  5669  wereu2  5672  xpdifid  6164  frpomin  6338  onfr  6400  onelssex  6409  ordunidif  6410  eliman0  6928  dffv2  6983  elrnrexdm  7087  eldmrexrn  7089  elabrex  7238  elunirn2OLD  7248  f1elima  7258  fliftfun  7305  fliftval  7309  f1oiso2  7345  sorpssuni  7718  sorpssint  7719  onssmin  7776  onminex  7786  fimaproj  8117  frxp2  8126  frxp3  8133  poseq  8140  tfrlem12  8385  seqomlem2  8447  oawordeulem  8550  oaass  8557  odi  8575  omass  8576  omeulem1  8578  oen0  8582  oelim2  8591  oeeulem  8597  nnawordex  8633  eldifsucnn  8659  cofon1  8667  cofon2  8668  naddcllem  8671  naddunif  8688  boxcutc  8931  snfi  9040  rexdif1en  9154  rexdif1enOLD  9155  findcard  9159  nnfi  9163  pssnn  9164  ssnnfiOLD  9166  unfi  9168  pwfir  9172  onfin  9226  pssnnOLD  9261  dif1ennnALT  9273  frfi  9284  fisupg  9287  nnsdomg  9298  nnsdomgOLD  9299  unfiOLD  9309  fissuni  9353  fipreima  9354  finsschain  9355  indexfi  9356  marypha1lem  9424  eqsup  9447  supmax  9458  fisup2g  9459  fisupcl  9460  supisoex  9465  infmin  9485  fiinfg  9490  fiinf2g  9491  wofib  9536  wemaplem2  9538  card2inf  9546  brwdom2  9564  cnfcom3clem  9696  ssttrcl  9706  ttrcltr  9707  trcl  9719  frmin  9740  r1ordg  9769  r1pwss  9775  tz9.12lem3  9780  tz9.12  9781  r1elwf  9787  tcrank  9875  scottex  9876  scott0  9877  isnumi  9937  onsdom  9987  ondomen  10028  infpwfien  10053  cardaleph  10080  infenaleph  10082  alephfplem4  10098  alephfp2  10100  dfac2b  10121  ackbij1lem18  10228  ackbij1  10229  cflem  10237  cflecard  10244  cfsuc  10248  cfflb  10250  cofsmo  10260  coftr  10264  fin23lem7  10307  fin23lem11  10308  enfin2i  10312  fin23lem26  10316  isf32lem5  10348  isf34lem4  10368  isfin1-3  10377  fin1a2lem7  10397  axdc3lem4  10444  ttukeylem7  10506  iunfo  10530  ficard  10556  pwcfsdom  10574  fpwwe2lem11  10632  wunex  10730  eltsk2g  10742  grur1  10811  axgroth6  10819  inaprc  10827  nqereu  10920  archnq  10971  genpnmax  10998  ltexpri  11034  prlem936  11038  recexpr  11042  supexpr  11045  negexsr  11093  recexsrlem  11094  recexsr  11098  supsrlem  11102  axrnegex  11153  axrrecex  11154  axpre-sup  11160  1re  11210  dedekind  11373  dedekindle  11374  cnegex  11391  cnegex2  11392  recex  11842  receu  11855  fiminre2  12158  cju  12204  nn2ge  12235  nominpos  12445  zdiv  12628  btwnz  12661  uzwo  12891  ublbneg  12913  lbzbi  12916  zsupss  12917  uzsupss  12920  rpnnen1lem1  12958  rpnnen1lem3  12959  rpnnen1lem4  12960  rpnnen1lem5  12961  z2ge  13173  qbtwnre  13174  qbtwnxr  13175  xralrple  13180  xrsupsslem  13282  xrinfmsslem  13283  supxrpnf  13293  icc0  13368  uzsup  13824  expnbnd  14191  expmulnbnd  14194  hashkf  14288  hashdom  14335  iswrdi  14464  rtrclreclem1  15000  rtrclreclem2  15002  rtrclreclem3  15003  01sqrex  15192  resqrex  15193  sqrtneg  15210  abs1m  15278  rexanuz  15288  rexuz3  15291  rexuzre  15295  sqreu  15303  o1lo1  15477  climconst  15483  rlimclim1  15485  climshftlem  15514  rlimo1  15557  lo1add  15567  lo1mul  15568  lo1le  15594  isercoll  15610  serf0  15623  zsum  15660  fsum  15662  fsumcvg3  15671  mertenslem1  15826  ntrivcvgn0  15840  ntrivcvgmullem  15843  zprod  15877  fprod  15881  fprodntriv  15882  dvdsval2  16196  dvds0lem  16206  dvds1lem  16207  dvds2lem  16208  odd2np1lem  16279  odd2np1  16280  opeo  16304  omeo  16305  divalglem9  16340  gcdcllem3  16438  lcmcllem  16529  qredeu  16591  exprmfct  16637  isprm5  16640  odzcllem  16721  reumodprminv  16733  modprm0  16734  nnnn0modprm0  16735  pythagtriplem19  16762  pcprmpw2  16811  pockthi  16836  infpnlem2  16840  vdwlem2  16911  vdwlem10  16919  vdwlem13  16922  ramub1lem1  16955  cshwrepswhash1  17032  imasleval  17483  mreexexlem3d  17586  mreexexlem4d  17587  iscatd  17613  cat1  18043  poslubd  18362  fpwipodrs  18489  ismgmid2  18583  mgmidsssn0  18587  gsumval2a  18600  ismndd  18643  isgrpd2  18838  isgrpd  18840  imasgrp2  18934  mhmmnd  18941  ghmgrp  18943  gaorber  19166  orbsta  19171  cayleyth  19277  pmtrdifel  19342  pmtrdifwrdel  19347  pmtrdifwrdel2  19348  psgnunilem2  19357  psgnunilem3  19358  psgnvalii  19371  pgpfi1  19457  sylow1lem3  19462  sylow1lem5  19464  pgpfi  19467  sylow2alem2  19480  efgredeu  19614  lt6abl  19757  pgpfac1lem3a  19940  pgpfac1lem3  19941  pgpfac1lem5  19943  pgpfaclem1  19945  pgpfaclem3  19947  ablfaclem2  19950  dvdsrmul  20170  dvdsr01  20177  irredrmul  20233  rhmdvdsr  20279  lspf  20577  lspval  20578  lssats2  20603  lspfixed  20733  lspsolvlem  20747  zringlpir  21028  zncyg  21095  cygth  21118  frlmup4  21347  aspval  21418  evlseu  21637  fiinbas  22446  topbas  22466  pptbas  22502  clsval  22532  elcls  22568  neiint  22599  neips  22608  opnneissb  22609  opnssneib  22610  innei  22620  neiptopnei  22627  restbas  22653  neitr  22675  pnfnei  22715  mnfnei  22716  lmconst  22756  iscnp4  22758  cncnpi  22773  cnconst2  22778  cnprest  22784  cnpdis  22788  nrmsep  22852  regsep2  22871  cmpcovf  22886  cmpsub  22895  cmpcld  22897  hauscmplem  22901  conncompid  22926  2ndci  22943  2ndcsb  22944  2ndc1stc  22946  1stcrest  22948  2ndcctbss  22950  2ndcdisj  22951  2ndcomap  22953  2ndcsep  22954  dis2ndc  22955  restlly  22978  islly2  22979  hausllycmp  22989  cldllycmp  22990  lly1stc  22991  dislly  22992  ssref  23007  refref  23008  finlocfin  23015  dissnlocfin  23024  locfindis  23025  llycmpkgen2  23045  cmpkgen  23046  1stckgenlem  23048  elptr  23068  ptbasfi  23076  neitx  23102  ptpjopn  23107  txcnp  23115  ptcnplem  23116  txlly  23131  txnlly  23132  txtube  23135  txcmplem1  23136  tx1stc  23145  txkgen  23147  xkococnlem  23154  txconn  23184  tgqtop  23207  kqreglem1  23236  kqreglem2  23237  kqnrmlem1  23238  kqnrmlem2  23239  reghmph  23288  nrmhmph  23289  fbssfi  23332  opnfbas  23337  isfil2  23351  fsubbas  23362  ssfg  23367  fgss2  23369  fbasrn  23379  filuni  23380  fgtr  23385  ssufl  23413  uffix  23416  elfm2  23443  elfm3  23445  imaelfm  23446  rnelfmlem  23447  rnelfm  23448  fmfnfmlem4  23452  fmfnfm  23453  fmco  23456  ufldom  23457  hausflim  23476  flimcls  23480  hauspwpwf1  23482  flffbas  23490  txflf  23501  fclscf  23520  fclsfnflim  23522  alexsubALTlem4  23545  alexsubALT  23546  tmdgsum2  23591  symgtgp  23601  subgntr  23602  opnsubg  23603  ghmcnp  23610  qustgpopn  23615  tsmsfbas  23623  tsmsxplem1  23648  ustexsym  23711  trust  23725  utoptop  23730  restutop  23733  restutopopn  23734  ustuqtop4  23740  utopsnneiplem  23743  iducn  23779  fmucnd  23788  cfilufg  23789  trcfilu  23790  neipcfilu  23792  imasdsf1olem  23870  blssps  23921  blss  23922  blssexps  23923  blssex  23924  ssblex  23925  blin2  23926  neibl  24001  blcld  24005  metss2  24012  stdbdmopn  24018  met1stc  24021  met2ndci  24022  metrest  24024  prdsxmslem2  24029  metcnp3  24040  metustexhalf  24056  metustfbas  24057  cfilucfil  24059  restmetu  24070  dscopn  24073  ngptgp  24136  nlmvscnlem1  24194  tgioo  24303  tgqioo  24307  xrsmopn  24319  zcld  24320  recld2  24321  zdis  24323  icccmplem1  24329  icccmplem2  24330  xmetdcn2  24344  addcnlem  24371  xrhmeo  24453  cnheibor  24462  cnllycmp  24463  lebnumlem3  24470  lebnum  24471  xlebnum  24472  lebnumii  24473  elpi1i  24553  ipcnlem1  24753  lmnn  24771  iscfil3  24781  cfilres  24804  flimcfil  24822  bcthlem4  24835  bcthlem5  24836  minveclem4c  24933  minveclem2  24934  minveclem3b  24936  minveclem3  24937  minveclem4  24940  minveclem6  24942  ivthlem2  24960  ivth  24962  ivthle  24964  ivthle2  24965  elovolmr  24984  ovolunlem1  25005  ovoliunlem2  25011  ovolicc1  25024  iundisj  25056  iunmbl2  25065  dyadmbllem  25107  volivth  25115  mbflimsup  25174  i1faddlem  25201  i1fmullem  25202  itg2lr  25239  itg2monolem1  25259  limcnlp  25386  ellimc3  25387  limcflf  25389  limciun  25402  rollelem  25497  c1lip1  25505  lhop1lem  25521  ply1divex  25645  ig1peu  25680  elply2  25701  coeeq  25732  plydivlem3  25799  plydivlem4  25800  elqaalem3  25825  qaa  25827  iaa  25829  aareccl  25830  aannenlem2  25833  aalioulem2  25837  aalioulem3  25838  aalioulem5  25840  aalioulem6  25841  aaliou  25842  aaliou2  25844  aaliou3lem8  25849  ulmshftlem  25892  reeff1o  25950  pilem2  25955  pilem3  25956  efif1olem2  26043  efopn  26157  cxpcn3lem  26244  cxpeq  26254  dcubic2  26338  quart  26355  xrlimcnp  26462  ftalem5  26570  ftalem7  26572  sgmnncl  26640  dvdsppwf1o  26679  musum  26684  perfect  26723  dchrptlem1  26756  dchrptlem2  26757  dchrpt  26759  bpos1lem  26774  lgsqrlem4  26841  lgsdchrval  26846  2sqblem  26923  dchrisumlem3  26983  chpdifbndlem2  27046  pntrsumbnd2  27059  pntpbnd1  27078  pntpbnd2  27079  pntpbnd  27080  pntibndlem2  27083  pntibndlem3  27084  pntleme  27100  pntlem3  27101  elno2  27146  sltval2  27148  noreson  27152  sltres  27154  noseponlem  27156  nolesgn2o  27163  nogesgn1o  27165  nodense  27184  nosupfv  27198  nosupres  27199  nosupbnd1lem3  27202  nosupbnd1lem5  27204  nosupbnd2lem1  27207  noinffv  27213  noinfres  27214  noinfbnd1lem3  27217  noinfbnd1lem5  27219  noinfbnd2lem1  27222  noetasuplem4  27228  noetainflem4  27232  noetalem2  27234  cuteq0  27322  cuteq1  27323  oldlim  27370  cofcutrtime  27403  cofss  27406  coiniss  27407  cutlt  27408  negsex  27506  negsfo  27516  norecdiv  27627  divs1  27640  precsexlem11  27652  precsex  27653  recsex  27654  axtgcont  27709  tgcgrxfr  27758  legid  27827  btwnleg  27828  leg0  27832  tghilberti1  27877  tglnpt2  27881  colline  27889  mirreu3  27894  isperp2  27955  colperpex  27973  lnopp2hpgb  28003  hpgerlem  28005  brbtwn  28146  brcgr  28147  brbtwn2  28152  axpasch  28188  axlowdimlem14  28202  axlowdim2  28207  axcontlem2  28212  axcontlem4  28214  axcontlem8  28218  axcontlem10  28220  axcontlem12  28222  fusgrn0degnn0  28745  friendshipgt3  29640  lpni  29720  isgrpoi  29738  vacn  29934  smcnlem  29937  nmosetn0  30005  nmoolb  30011  nmobndi  30015  nmoo0  30031  nmlno0lem  30033  isblo3i  30041  blo3i  30042  blocnilem  30044  ubthlem1  30110  minvecolem2  30115  minvecolem3  30116  minvecolem4c  30119  minvecolem4  30120  minvecolem5  30121  minvecolem6  30122  norm1exi  30490  occl  30544  spanval  30573  spancl  30576  shsval2i  30627  ococin  30648  pjoml6i  30829  nmopsetn0  31105  nmfnsetn0  31118  nmoplb  31147  nmfnlb  31164  nmop0  31226  nmfn0  31227  nmlnop0iALT  31235  nmopun  31254  nmcexi  31266  lnconi  31273  lnopcnbd  31276  lnfncnbd  31297  riesz3i  31302  riesz1  31305  cnlnadjlem2  31308  cnlnadjlem8  31314  cnlnadjlem9  31315  adjbd1o  31325  branmfn  31345  opsqrlem1  31380  pjnmopi  31388  strlem1  31490  stri  31497  hstri  31505  cvcon3  31524  cvnbtwn  31526  superpos  31594  shatomici  31598  atcvat4i  31637  mdsymlem2  31644  cdj1i  31673  cdj3i  31681  rexunirn  31719  foresf1o  31729  iundisjf  31807  aciunf1lem  31874  fnpreimac  31883  fgreu  31884  fcnvgreu  31885  xrge0infss  31960  ssnnssfz  31985  iundisjfi  31994  xreceu  32075  rexdiv  32079  isarchi3  32320  archirngz  32322  archiabllem2a  32327  0nellinds  32471  qtophaus  32804  reff  32807  locfinreflem  32808  cmpcref  32818  dispcmp  32827  tpr2rico  32880  pnfneige0  32919  qqhucn  32960  rrhre  32989  indf1ofs  33012  esumcst  33049  esumpcvgval  33064  dmsigagen  33130  rossros  33166  dya2icoseg  33264  dya2iocnrect  33268  dya2iocuni  33270  eulerpartlemgvv  33363  dstfrvunirn  33461  ballotlem4  33485  ballotlemic  33493  ballotlem1c  33494  ballotlemrc  33517  signsw0g  33555  signswmnd  33556  prodfzo03  33603  tgoldbachgt  33663  loop1cycl  34116  umgr2cycllem  34119  umgr2cycl  34120  subfacp1lem3  34161  erdsze2lem2  34183  cnpconn  34209  txpconn  34211  ptpconn  34212  indispconn  34213  connpconn  34214  cvxpconn  34221  cnllysconn  34224  cvmsss2  34253  cvmcov2  34254  cvmopnlem  34257  cvmliftlem14  34276  cvmliftlem15  34277  cvmlift2lem11  34292  cvmlift2lem12  34293  cvmlift2lem13  34294  cvmlift3lem2  34299  cvmlift3lem6  34303  cvmlift3lem9  34306  mthmi  34556  br8  34714  br6  34715  br4  34716  dfon2lem9  34751  wzel  34784  wsuclem  34785  wsuclb  34788  imagesset  34913  fvtransport  34992  brcolinear  35019  brsegle  35068  seglerflx  35072  seglemin  35073  btwnsegle  35077  fvray  35101  fvline  35104  hilbert1.1  35114  elhf2  35135  0hf  35137  nn0prpwlem  35195  nn0prpw  35196  fness  35222  fneref  35223  fnessref  35230  refssfne  35231  neibastop2lem  35233  fnemeet1  35239  tailfb  35250  filnetlem4  35254  limsucncmpi  35318  taupilemrplb  36189  relowlssretop  36232  rdgellim  36245  matunitlindflem2  36473  ptrecube  36476  poimirlem4  36480  poimirlem17  36493  poimirlem20  36496  poimirlem23  36499  poimirlem24  36500  poimirlem26  36502  poimirlem27  36503  poimirlem29  36505  poimirlem32  36508  heicant  36511  mblfinlem1  36513  mblfinlem2  36514  mblfinlem3  36515  mblfinlem4  36516  ismblfin  36517  volsupnfl  36521  itg2addnclem  36527  itg2addnclem3  36529  itg2addnc  36530  ftc1anclem5  36553  unirep  36570  cover2  36571  indexa  36589  frinfm  36591  sdclem1  36599  fdc  36601  incsequz  36604  caushft  36617  istotbnd3  36627  0totbnd  36629  sstotbnd2  36630  sstotbnd  36631  sstotbnd3  36632  isbnd3  36640  ssbnd  36644  equivbnd  36646  prdsbnd  36649  prdstotbnd  36650  cntotbnd  36652  heibor1lem  36665  heiborlem1  36667  heiborlem3  36669  heiborlem6  36672  heiborlem8  36674  bfplem2  36679  rrncmslem  36688  iccbnd  36696  opidonOLD  36708  exidres  36734  isrngod  36754  isgrpda  36811  isdrngo2  36814  igenval  36917  igenidl  36919  prtlem10  37723  lshpnel2N  37843  lsmsat  37866  lssatomic  37869  lcvnbtwn  37883  lfl1  37928  eqlkr  37957  lshpkrlem1  37968  lshpkrex  37976  cvrcon3b  38135  cvrat4  38302  3dim3  38328  ps-2  38337  llni  38367  llnle  38377  lplni  38391  lplnle  38399  lplnexllnN  38423  lvoli  38434  lnatexN  38638  elpaddn0  38659  pclfinN  38759  lhprelat3N  38899  4atexlemex2  38930  4atex  38935  4atex2-0aOLDN  38937  4atex2-0cOLDN  38939  lautcvr  38951  cdleme0ex1N  39082  cdleme50rnlem  39403  cdleme50ex  39418  cdlemg1cex  39447  cdlemkid5  39794  cdlemk  39833  tendoex  39834  cdleml5N  39839  cdlemm10N  39977  dih1dimatlem0  40187  dihjat1lem  40287  dvh3dim2  40307  dvh3dim3N  40308  dochkr1  40337  dochkr1OLDN  40338  lcfrvalsnN  40400  lcfrlem27  40428  lcfrlem37  40438  lcfr  40444  mapd1o  40507  mapdpglem23  40553  hdmap11lem2  40701  rspcedvdw  41025  resubeu  41246  nacsfix  41435  mzpcompact2lem  41474  eldioph  41481  diophrw  41482  diophin  41495  rexrabdioph  41517  rexzrexnn0  41527  eldioph4b  41534  rencldnfilem  41543  irrapxlem5  41549  irrapxlem6  41550  pell1234qrdich  41584  pell14qrdich  41592  infmrgelbi  41601  pellqrex  41602  pellfundre  41604  pellfundlb  41607  rmxynorm  41642  congrep  41697  acongrep  41704  jm2.27  41732  fnwe2lem2  41778  islssfgi  41799  hbtlem2  41851  hbtlem4  41853  hbtlem5  41855  dgraaub  41875  mpaaeu  41877  aaitgo  41889  rgspnval  41895  rgspncl  41896  unielss  41952  onexgt  41974  onexomgt  41975  onexlimgt  41977  onexoegt  41978  oaordnr  42031  omnord1  42040  oenord1  42051  oaomoencom  42052  oenass  42054  tfsconcatfv2  42075  tfsconcatrn  42077  tfsconcatb0  42079  ofoafo  42091  naddcnffo  42099  oaun3lem1  42109  naddwordnexlem4  42137  sucomisnotcard  42280  clsk1independent  42782  elabrexg  43713  restuni3  43792  iinssd  43805  founiiun  43860  wessf1ornlem  43867  founiiun0  43873  unirnmap  43892  dstregt0  43977  uzfissfz  44022  rpgtrecnn  44076  rexabslelem  44114  infrnmptle  44119  infxrunb3rnmpt  44124  infxrpnf  44142  supminfxr  44160  rexanuz2nf  44189  iooiinicc  44241  iooiinioc  44255  uzubioo  44266  climsuse  44310  islptre  44321  limsuppnfdlem  44403  climinf3  44418  limsupmnfuzlem  44428  limsupre3lem  44434  limsupre3uzlem  44437  0cnv  44444  liminfreuzlem  44504  cnrefiisplem  44531  icccncfext  44589  cncficcgt0  44590  dvbdfbdioo  44632  ioodvbdlimc1lem1  44633  ioodvbdlimc1lem2  44634  ioodvbdlimc2lem  44636  stoweidlem9  44711  stoweidlem14  44716  stoweidlem18  44720  stoweidlem21  44723  stoweidlem29  44731  stoweidlem34  44736  stoweidlem35  44737  stoweidlem39  44741  stoweidlem41  44743  stoweidlem45  44747  stoweidlem52  44754  stoweidlem55  44757  stoweidlem57  44759  stoweidlem60  44762  stirlinglem5  44780  stirlinglem13  44788  stirlinglem14  44789  fourierdlem16  44825  fourierdlem20  44829  fourierdlem21  44830  fourierdlem22  44831  fourierdlem25  44834  fourierdlem31  44840  fourierdlem39  44848  fourierdlem41  44850  fourierdlem42  44851  fourierdlem47  44855  fourierdlem48  44856  fourierdlem49  44857  fourierdlem51  44859  fourierdlem63  44871  fourierdlem64  44872  fourierdlem65  44873  fourierdlem77  44885  fourierdlem81  44889  fourierdlem83  44891  fourierdlem103  44911  fourierdlem104  44912  elaa2lem  44935  etransclem47  44983  qndenserrnbl  44997  ioorrnopnlem  45006  ioorrnopnxrlem  45008  intsaluni  45031  salgencntex  45045  subsaliuncllem  45059  sge0resplit  45108  sge0seq  45148  sge0reuz  45149  nnfoctbdjlem  45157  meaiininclem  45188  hoicvrrex  45258  ovnlecvr  45260  ovnlerp  45264  hoidmv1lelem2  45294  hoidmvlelem2  45298  hoidmvlelem3  45299  ovnhoilem1  45303  ovnlecvr2  45312  hoiqssbl  45327  ovolval4lem2  45352  ovolval5lem2  45355  ovnovollem1  45358  ovnovollem2  45359  iinhoiicclem  45375  smfinflem  45519  smflimsuplem7  45528  sprsymrelfolem2  46147  perfectALTV  46377  9gbo  46428  11gbo  46429  nnsum3primes4  46442  nnsum3primesprm  46444  ssnn0ssfz  46978  lincsumcl  47065  lincscmcl  47066  zlmodzxzldep  47138  ldepsnlinc  47142  line2ylem  47390  line2xlem  47392  rspceb2dv  47441  sepfsepc  47513  lubsscl  47546  glbsscl  47547  aacllem  47801