Theorem rspcev 3613

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072

This theorem is referenced by:  rspcedvdw  3616  rspceaimv  3618  rspc2ev  3625  rspc3ev  3629  rspceeqv  3634  reu6i  3725  rspesbca  3876  eliuni  5004  iuneqconst  5009  brralrspcev  5209  wefrc  5671  wereu2  5674  xpdifid  6168  frpomin  6342  onfr  6404  onelssex  6413  ordunidif  6414  eliman0  6932  dffv2  6987  elrnrexdm  7091  eldmrexrn  7093  elabrex  7242  elunirn2OLD  7252  f1elima  7262  fliftfun  7309  fliftval  7313  f1oiso2  7349  sorpssuni  7722  sorpssint  7723  onssmin  7780  onminex  7790  fimaproj  8121  frxp2  8130  frxp3  8137  poseq  8144  tfrlem12  8389  seqomlem2  8451  oawordeulem  8554  oaass  8561  odi  8579  omass  8580  omeulem1  8582  oen0  8586  oelim2  8595  oeeulem  8601  nnawordex  8637  eldifsucnn  8663  cofon1  8671  cofon2  8672  naddcllem  8675  naddunif  8692  boxcutc  8935  snfi  9044  rexdif1en  9158  rexdif1enOLD  9159  findcard  9163  nnfi  9167  pssnn  9168  ssnnfiOLD  9170  unfi  9172  pwfir  9176  onfin  9230  pssnnOLD  9265  dif1ennnALT  9277  frfi  9288  fisupg  9291  nnsdomg  9302  nnsdomgOLD  9303  unfiOLD  9313  fissuni  9357  fipreima  9358  finsschain  9359  indexfi  9360  marypha1lem  9428  eqsup  9451  supmax  9462  fisup2g  9463  fisupcl  9464  supisoex  9469  infmin  9489  fiinfg  9494  fiinf2g  9495  wofib  9540  wemaplem2  9542  card2inf  9550  brwdom2  9568  cnfcom3clem  9700  ssttrcl  9710  ttrcltr  9711  trcl  9723  frmin  9744  r1ordg  9773  r1pwss  9779  tz9.12lem3  9784  tz9.12  9785  r1elwf  9791  tcrank  9879  scottex  9880  scott0  9881  isnumi  9941  onsdom  9991  ondomen  10032  infpwfien  10057  cardaleph  10084  infenaleph  10086  alephfplem4  10102  alephfp2  10104  dfac2b  10125  ackbij1lem18  10232  ackbij1  10233  cflem  10241  cflecard  10248  cfsuc  10252  cfflb  10254  cofsmo  10264  coftr  10268  fin23lem7  10311  fin23lem11  10312  enfin2i  10316  fin23lem26  10320  isf32lem5  10352  isf34lem4  10372  isfin1-3  10381  fin1a2lem7  10401  axdc3lem4  10448  ttukeylem7  10510  iunfo  10534  ficard  10560  pwcfsdom  10578  fpwwe2lem11  10636  wunex  10734  eltsk2g  10746  grur1  10815  axgroth6  10823  inaprc  10831  nqereu  10924  archnq  10975  genpnmax  11002  ltexpri  11038  prlem936  11042  recexpr  11046  supexpr  11049  negexsr  11097  recexsrlem  11098  recexsr  11102  supsrlem  11106  axrnegex  11157  axrrecex  11158  axpre-sup  11164  1re  11214  dedekind  11377  dedekindle  11378  cnegex  11395  cnegex2  11396  recex  11846  receu  11859  fiminre2  12162  cju  12208  nn2ge  12239  nominpos  12449  zdiv  12632  btwnz  12665  uzwo  12895  ublbneg  12917  lbzbi  12920  zsupss  12921  uzsupss  12924  rpnnen1lem1  12962  rpnnen1lem3  12963  rpnnen1lem4  12964  rpnnen1lem5  12965  z2ge  13177  qbtwnre  13178  qbtwnxr  13179  xralrple  13184  xrsupsslem  13286  xrinfmsslem  13287  supxrpnf  13297  icc0  13372  uzsup  13828  expnbnd  14195  expmulnbnd  14198  hashkf  14292  hashdom  14339  iswrdi  14468  rtrclreclem1  15004  rtrclreclem2  15006  rtrclreclem3  15007  01sqrex  15196  resqrex  15197  sqrtneg  15214  abs1m  15282  rexanuz  15292  rexuz3  15295  rexuzre  15299  sqreu  15307  o1lo1  15481  climconst  15487  rlimclim1  15489  climshftlem  15518  rlimo1  15561  lo1add  15571  lo1mul  15572  lo1le  15598  isercoll  15614  serf0  15627  zsum  15664  fsum  15666  fsumcvg3  15675  mertenslem1  15830  ntrivcvgn0  15844  ntrivcvgmullem  15847  zprod  15881  fprod  15885  fprodntriv  15886  dvdsval2  16200  dvds0lem  16210  dvds1lem  16211  dvds2lem  16212  odd2np1lem  16283  odd2np1  16284  opeo  16308  omeo  16309  divalglem9  16344  gcdcllem3  16442  lcmcllem  16533  qredeu  16595  exprmfct  16641  isprm5  16644  odzcllem  16725  reumodprminv  16737  modprm0  16738  nnnn0modprm0  16739  pythagtriplem19  16766  pcprmpw2  16815  pockthi  16840  infpnlem2  16844  vdwlem2  16915  vdwlem10  16923  vdwlem13  16926  ramub1lem1  16959  cshwrepswhash1  17036  imasleval  17487  mreexexlem3d  17590  mreexexlem4d  17591  iscatd  17617  cat1  18047  poslubd  18366  fpwipodrs  18493  ismgmid2  18587  mgmidsssn0  18591  gsumval2a  18604  ismndd  18647  isgrpd2  18842  isgrpd  18844  imasgrp2  18938  mhmmnd  18947  ghmgrp  18949  gaorber  19172  orbsta  19177  cayleyth  19283  pmtrdifel  19348  pmtrdifwrdel  19353  pmtrdifwrdel2  19354  psgnunilem2  19363  psgnunilem3  19364  psgnvalii  19377  pgpfi1  19463  sylow1lem3  19468  sylow1lem5  19470  pgpfi  19473  sylow2alem2  19486  efgredeu  19620  lt6abl  19763  pgpfac1lem3a  19946  pgpfac1lem3  19947  pgpfac1lem5  19949  pgpfaclem1  19951  pgpfaclem3  19953  ablfaclem2  19956  dvdsrmul  20178  dvdsr01  20185  irredrmul  20241  rhmdvdsr  20287  lspf  20585  lspval  20586  lssats2  20611  lspfixed  20741  lspsolvlem  20755  zringlpir  21037  zncyg  21104  cygth  21127  frlmup4  21356  aspval  21427  evlseu  21646  fiinbas  22455  topbas  22475  pptbas  22511  clsval  22541  elcls  22577  neiint  22608  neips  22617  opnneissb  22618  opnssneib  22619  innei  22629  neiptopnei  22636  restbas  22662  neitr  22684  pnfnei  22724  mnfnei  22725  lmconst  22765  iscnp4  22767  cncnpi  22782  cnconst2  22787  cnprest  22793  cnpdis  22797  nrmsep  22861  regsep2  22880  cmpcovf  22895  cmpsub  22904  cmpcld  22906  hauscmplem  22910  conncompid  22935  2ndci  22952  2ndcsb  22953  2ndc1stc  22955  1stcrest  22957  2ndcctbss  22959  2ndcdisj  22960  2ndcomap  22962  2ndcsep  22963  dis2ndc  22964  restlly  22987  islly2  22988  hausllycmp  22998  cldllycmp  22999  lly1stc  23000  dislly  23001  ssref  23016  refref  23017  finlocfin  23024  dissnlocfin  23033  locfindis  23034  llycmpkgen2  23054  cmpkgen  23055  1stckgenlem  23057  elptr  23077  ptbasfi  23085  neitx  23111  ptpjopn  23116  txcnp  23124  ptcnplem  23125  txlly  23140  txnlly  23141  txtube  23144  txcmplem1  23145  tx1stc  23154  txkgen  23156  xkococnlem  23163  txconn  23193  tgqtop  23216  kqreglem1  23245  kqreglem2  23246  kqnrmlem1  23247  kqnrmlem2  23248  reghmph  23297  nrmhmph  23298  fbssfi  23341  opnfbas  23346  isfil2  23360  fsubbas  23371  ssfg  23376  fgss2  23378  fbasrn  23388  filuni  23389  fgtr  23394  ssufl  23422  uffix  23425  elfm2  23452  elfm3  23454  imaelfm  23455  rnelfmlem  23456  rnelfm  23457  fmfnfmlem4  23461  fmfnfm  23462  fmco  23465  ufldom  23466  hausflim  23485  flimcls  23489  hauspwpwf1  23491  flffbas  23499  txflf  23510  fclscf  23529  fclsfnflim  23531  alexsubALTlem4  23554  alexsubALT  23555  tmdgsum2  23600  symgtgp  23610  subgntr  23611  opnsubg  23612  ghmcnp  23619  qustgpopn  23624  tsmsfbas  23632  tsmsxplem1  23657  ustexsym  23720  trust  23734  utoptop  23739  restutop  23742  restutopopn  23743  ustuqtop4  23749  utopsnneiplem  23752  iducn  23788  fmucnd  23797  cfilufg  23798  trcfilu  23799  neipcfilu  23801  imasdsf1olem  23879  blssps  23930  blss  23931  blssexps  23932  blssex  23933  ssblex  23934  blin2  23935  neibl  24010  blcld  24014  metss2  24021  stdbdmopn  24027  met1stc  24030  met2ndci  24031  metrest  24033  prdsxmslem2  24038  metcnp3  24049  metustexhalf  24065  metustfbas  24066  cfilucfil  24068  restmetu  24079  dscopn  24082  ngptgp  24145  nlmvscnlem1  24203  tgioo  24312  tgqioo  24316  xrsmopn  24328  zcld  24329  recld2  24330  zdis  24332  icccmplem1  24338  icccmplem2  24339  xmetdcn2  24353  addcnlem  24380  xrhmeo  24462  cnheibor  24471  cnllycmp  24472  lebnumlem3  24479  lebnum  24480  xlebnum  24481  lebnumii  24482  elpi1i  24562  ipcnlem1  24762  lmnn  24780  iscfil3  24790  cfilres  24813  flimcfil  24831  bcthlem4  24844  bcthlem5  24845  minveclem4c  24942  minveclem2  24943  minveclem3b  24945  minveclem3  24946  minveclem4  24949  minveclem6  24951  ivthlem2  24969  ivth  24971  ivthle  24973  ivthle2  24974  elovolmr  24993  ovolunlem1  25014  ovoliunlem2  25020  ovolicc1  25033  iundisj  25065  iunmbl2  25074  dyadmbllem  25116  volivth  25124  mbflimsup  25183  i1faddlem  25210  i1fmullem  25211  itg2lr  25248  itg2monolem1  25268  limcnlp  25395  ellimc3  25396  limcflf  25398  limciun  25411  rollelem  25506  c1lip1  25514  lhop1lem  25530  ply1divex  25654  ig1peu  25689  elply2  25710  coeeq  25741  plydivlem3  25808  plydivlem4  25809  elqaalem3  25834  qaa  25836  iaa  25838  aareccl  25839  aannenlem2  25842  aalioulem2  25846  aalioulem3  25847  aalioulem5  25849  aalioulem6  25850  aaliou  25851  aaliou2  25853  aaliou3lem8  25858  ulmshftlem  25901  reeff1o  25959  pilem2  25964  pilem3  25965  efif1olem2  26052  efopn  26166  cxpcn3lem  26255  cxpeq  26265  dcubic2  26349  quart  26366  xrlimcnp  26473  ftalem5  26581  ftalem7  26583  sgmnncl  26651  dvdsppwf1o  26690  musum  26695  perfect  26734  dchrptlem1  26767  dchrptlem2  26768  dchrpt  26770  bpos1lem  26785  lgsqrlem4  26852  lgsdchrval  26857  2sqblem  26934  dchrisumlem3  26994  chpdifbndlem2  27057  pntrsumbnd2  27070  pntpbnd1  27089  pntpbnd2  27090  pntpbnd  27091  pntibndlem2  27094  pntibndlem3  27095  pntleme  27111  pntlem3  27112  elno2  27157  sltval2  27159  noreson  27163  sltres  27165  noseponlem  27167  nolesgn2o  27174  nogesgn1o  27176  nodense  27195  nosupfv  27209  nosupres  27210  nosupbnd1lem3  27213  nosupbnd1lem5  27215  nosupbnd2lem1  27218  noinffv  27224  noinfres  27225  noinfbnd1lem3  27228  noinfbnd1lem5  27230  noinfbnd2lem1  27233  noetasuplem4  27239  noetainflem4  27243  noetalem2  27245  cuteq0  27334  cuteq1  27335  oldlim  27382  cofcutrtime  27416  cofss  27419  coiniss  27420  cutlt  27421  negsex  27520  negsfo  27530  norecdiv  27641  divs1  27654  precsexlem11  27666  precsex  27667  recsex  27668  elons2d  27689  n0ons  27708  axtgcont  27751  tgcgrxfr  27800  legid  27869  btwnleg  27870  leg0  27874  tghilberti1  27919  tglnpt2  27923  colline  27931  mirreu3  27936  isperp2  27997  colperpex  28015  lnopp2hpgb  28045  hpgerlem  28047  brbtwn  28188  brcgr  28189  brbtwn2  28194  axpasch  28230  axlowdimlem14  28244  axlowdim2  28249  axcontlem2  28254  axcontlem4  28256  axcontlem8  28260  axcontlem10  28262  axcontlem12  28264  fusgrn0degnn0  28787  friendshipgt3  29682  lpni  29764  isgrpoi  29782  vacn  29978  smcnlem  29981  nmosetn0  30049  nmoolb  30055  nmobndi  30059  nmoo0  30075  nmlno0lem  30077  isblo3i  30085  blo3i  30086  blocnilem  30088  ubthlem1  30154  minvecolem2  30159  minvecolem3  30160  minvecolem4c  30163  minvecolem4  30164  minvecolem5  30165  minvecolem6  30166  norm1exi  30534  occl  30588  spanval  30617  spancl  30620  shsval2i  30671  ococin  30692  pjoml6i  30873  nmopsetn0  31149  nmfnsetn0  31162  nmoplb  31191  nmfnlb  31208  nmop0  31270  nmfn0  31271  nmlnop0iALT  31279  nmopun  31298  nmcexi  31310  lnconi  31317  lnopcnbd  31320  lnfncnbd  31341  riesz3i  31346  riesz1  31349  cnlnadjlem2  31352  cnlnadjlem8  31358  cnlnadjlem9  31359  adjbd1o  31369  branmfn  31389  opsqrlem1  31424  pjnmopi  31432  strlem1  31534  stri  31541  hstri  31549  cvcon3  31568  cvnbtwn  31570  superpos  31638  shatomici  31642  atcvat4i  31681  mdsymlem2  31688  cdj1i  31717  cdj3i  31725  rexunirn  31763  foresf1o  31773  iundisjf  31851  aciunf1lem  31918  fnpreimac  31927  fgreu  31928  fcnvgreu  31929  xrge0infss  32004  ssnnssfz  32029  iundisjfi  32038  xreceu  32119  rexdiv  32123  isarchi3  32364  archirngz  32366  archiabllem2a  32371  0nellinds  32514  qtophaus  32847  reff  32850  locfinreflem  32851  cmpcref  32861  dispcmp  32870  tpr2rico  32923  pnfneige0  32962  qqhucn  33003  rrhre  33032  indf1ofs  33055  esumcst  33092  esumpcvgval  33107  dmsigagen  33173  rossros  33209  dya2icoseg  33307  dya2iocnrect  33311  dya2iocuni  33313  eulerpartlemgvv  33406  dstfrvunirn  33504  ballotlem4  33528  ballotlemic  33536  ballotlem1c  33537  ballotlemrc  33560  signsw0g  33598  signswmnd  33599  prodfzo03  33646  tgoldbachgt  33706  loop1cycl  34159  umgr2cycllem  34162  umgr2cycl  34163  subfacp1lem3  34204  erdsze2lem2  34226  cnpconn  34252  txpconn  34254  ptpconn  34255  indispconn  34256  connpconn  34257  cvxpconn  34264  cnllysconn  34267  cvmsss2  34296  cvmcov2  34297  cvmopnlem  34300  cvmliftlem14  34319  cvmliftlem15  34320  cvmlift2lem11  34335  cvmlift2lem12  34336  cvmlift2lem13  34337  cvmlift3lem2  34342  cvmlift3lem6  34346  cvmlift3lem9  34349  mthmi  34599  br8  34757  br6  34758  br4  34759  dfon2lem9  34794  wzel  34827  wsuclem  34828  wsuclb  34831  imagesset  34956  fvtransport  35035  brcolinear  35062  brsegle  35111  seglerflx  35115  seglemin  35116  btwnsegle  35120  fvray  35144  fvline  35147  hilbert1.1  35157  elhf2  35178  0hf  35180  nn0prpwlem  35255  nn0prpw  35256  fness  35282  fneref  35283  fnessref  35290  refssfne  35291  neibastop2lem  35293  fnemeet1  35299  tailfb  35310  filnetlem4  35314  limsucncmpi  35378  taupilemrplb  36249  relowlssretop  36292  rdgellim  36305  matunitlindflem2  36533  ptrecube  36536  poimirlem4  36540  poimirlem17  36553  poimirlem20  36556  poimirlem23  36559  poimirlem24  36560  poimirlem26  36562  poimirlem27  36563  poimirlem29  36565  poimirlem32  36568  heicant  36571  mblfinlem1  36573  mblfinlem2  36574  mblfinlem3  36575  mblfinlem4  36576  ismblfin  36577  volsupnfl  36581  itg2addnclem  36587  itg2addnclem3  36589  itg2addnc  36590  ftc1anclem5  36613  unirep  36630  cover2  36631  indexa  36649  frinfm  36651  sdclem1  36659  fdc  36661  incsequz  36664  caushft  36677  istotbnd3  36687  0totbnd  36689  sstotbnd2  36690  sstotbnd  36691  sstotbnd3  36692  isbnd3  36700  ssbnd  36704  equivbnd  36706  prdsbnd  36709  prdstotbnd  36710  cntotbnd  36712  heibor1lem  36725  heiborlem1  36727  heiborlem3  36729  heiborlem6  36732  heiborlem8  36734  bfplem2  36739  rrncmslem  36748  iccbnd  36756  opidonOLD  36768  exidres  36794  isrngod  36814  isgrpda  36871  isdrngo2  36874  igenval  36977  igenidl  36979  prtlem10  37783  lshpnel2N  37903  lsmsat  37926  lssatomic  37929  lcvnbtwn  37943  lfl1  37988  eqlkr  38017  lshpkrlem1  38028  lshpkrex  38036  cvrcon3b  38195  cvrat4  38362  3dim3  38388  ps-2  38397  llni  38427  llnle  38437  lplni  38451  lplnle  38459  lplnexllnN  38483  lvoli  38494  lnatexN  38698  elpaddn0  38719  pclfinN  38819  lhprelat3N  38959  4atexlemex2  38990  4atex  38995  4atex2-0aOLDN  38997  4atex2-0cOLDN  38999  lautcvr  39011  cdleme0ex1N  39142  cdleme50rnlem  39463  cdleme50ex  39478  cdlemg1cex  39507  cdlemkid5  39854  cdlemk  39893  tendoex  39894  cdleml5N  39899  cdlemm10N  40037  dih1dimatlem0  40247  dihjat1lem  40347  dvh3dim2  40367  dvh3dim3N  40368  dochkr1  40397  dochkr1OLDN  40398  lcfrvalsnN  40460  lcfrlem27  40488  lcfrlem37  40498  lcfr  40504  mapd1o  40567  mapdpglem23  40613  hdmap11lem2  40761  resubeu  41298  nacsfix  41498  mzpcompact2lem  41537  eldioph  41544  diophrw  41545  diophin  41558  rexrabdioph  41580  rexzrexnn0  41590  eldioph4b  41597  rencldnfilem  41606  irrapxlem5  41612  irrapxlem6  41613  pell1234qrdich  41647  pell14qrdich  41655  infmrgelbi  41664  pellqrex  41665  pellfundre  41667  pellfundlb  41670  rmxynorm  41705  congrep  41760  acongrep  41767  jm2.27  41795  fnwe2lem2  41841  islssfgi  41862  hbtlem2  41914  hbtlem4  41916  hbtlem5  41918  dgraaub  41938  mpaaeu  41940  aaitgo  41952  rgspnval  41958  rgspncl  41959  unielss  42015  onexgt  42037  onexomgt  42038  onexlimgt  42040  onexoegt  42041  oaordnr  42094  omnord1  42103  oenord1  42114  oaomoencom  42115  oenass  42117  tfsconcatfv2  42138  tfsconcatrn  42140  tfsconcatb0  42142  ofoafo  42154  naddcnffo  42162  oaun3lem1  42172  naddwordnexlem4  42200  sucomisnotcard  42343  clsk1independent  42845  elabrexg  43776  restuni3  43855  iinssd  43868  founiiun  43923  wessf1ornlem  43930  founiiun0  43936  unirnmap  43955  dstregt0  44039  uzfissfz  44084  rpgtrecnn  44138  rexabslelem  44176  infrnmptle  44181  infxrunb3rnmpt  44186  infxrpnf  44204  supminfxr  44222  rexanuz2nf  44251  iooiinicc  44303  iooiinioc  44317  uzubioo  44328  climsuse  44372  islptre  44383  limsuppnfdlem  44465  climinf3  44480  limsupmnfuzlem  44490  limsupre3lem  44496  limsupre3uzlem  44499  0cnv  44506  liminfreuzlem  44566  cnrefiisplem  44593  icccncfext  44651  cncficcgt0  44652  dvbdfbdioo  44694  ioodvbdlimc1lem1  44695  ioodvbdlimc1lem2  44696  ioodvbdlimc2lem  44698  stoweidlem9  44773  stoweidlem14  44778  stoweidlem18  44782  stoweidlem21  44785  stoweidlem29  44793  stoweidlem34  44798  stoweidlem35  44799  stoweidlem39  44803  stoweidlem41  44805  stoweidlem45  44809  stoweidlem52  44816  stoweidlem55  44819  stoweidlem57  44821  stoweidlem60  44824  stirlinglem5  44842  stirlinglem13  44850  stirlinglem14  44851  fourierdlem16  44887  fourierdlem20  44891  fourierdlem21  44892  fourierdlem22  44893  fourierdlem25  44896  fourierdlem31  44902  fourierdlem39  44910  fourierdlem41  44912  fourierdlem42  44913  fourierdlem47  44917  fourierdlem48  44918  fourierdlem49  44919  fourierdlem51  44921  fourierdlem63  44933  fourierdlem64  44934  fourierdlem65  44935  fourierdlem77  44947  fourierdlem81  44951  fourierdlem83  44953  fourierdlem103  44973  fourierdlem104  44974  elaa2lem  44997  etransclem47  45045  qndenserrnbl  45059  ioorrnopnlem  45068  ioorrnopnxrlem  45070  intsaluni  45093  salgencntex  45107  subsaliuncllem  45121  sge0resplit  45170  sge0seq  45210  sge0reuz  45211  nnfoctbdjlem  45219  meaiininclem  45250  hoicvrrex  45320  ovnlecvr  45322  ovnlerp  45326  hoidmv1lelem2  45356  hoidmvlelem2  45360  hoidmvlelem3  45361  ovnhoilem1  45365  ovnlecvr2  45374  hoiqssbl  45389  ovolval4lem2  45414  ovolval5lem2  45417  ovnovollem1  45420  ovnovollem2  45421  iinhoiicclem  45437  smfinflem  45581  smflimsuplem7  45590  sprsymrelfolem2  46209  perfectALTV  46439  9gbo  46490  11gbo  46491  nnsum3primes4  46504  nnsum3primesprm  46506  pzriprnglem13  46865  ssnn0ssfz  47073  lincsumcl  47160  lincscmcl  47161  zlmodzxzldep  47233  ldepsnlinc  47237  line2ylem  47485  line2xlem  47487  rspceb2dv  47536  sepfsepc  47608  lubsscl  47641  glbsscl  47642  aacllem  47896