Theorem rspcev 3635

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077

This theorem is referenced by:  rspcedvdw  3638  rspceb2dv  3639  rspceaimv  3641  rspc2ev  3648  rspc3ev  3652  rspceeqv  3658  reu6i  3750  rspesbca  3903  eliuni  5021  iuneqconst  5026  brralrspcev  5226  wefrc  5694  wereu2  5697  xpdifid  6199  frpomin  6372  onfr  6434  onelssex  6443  ordunidif  6444  eliman0  6960  dffv2  7017  elrnrexdm  7123  eldmrexrn  7125  elabrex  7279  elabrexg  7280  elunirn2OLD  7290  f1elima  7300  fliftfun  7348  fliftval  7352  f1oiso2  7388  sorpssuni  7767  sorpssint  7768  onssmin  7828  onminex  7838  fimaproj  8176  frxp3  8192  poseq  8199  tfrlem12  8445  seqomlem2  8507  oawordeulem  8610  oaass  8617  odi  8635  omass  8636  omeulem1  8638  oen0  8642  oelim2  8651  oeeulem  8657  nnawordex  8693  nnaordex2  8695  eldifsucnn  8720  cofon1  8728  cofon2  8729  naddcllem  8732  naddunif  8749  boxcutc  8999  0fi  9108  snfi  9109  snfiOLD  9110  rexdif1en  9224  rexdif1enOLD  9225  findcard  9229  nnfi  9233  pssnn  9234  ssnnfiOLD  9236  unfi  9238  onfin  9293  dif1ennnALT  9339  frfi  9349  fisupg  9352  nnsdomg  9363  nnsdomgOLD  9364  pwfir  9383  prfi  9391  fissuni  9427  fipreima  9428  finsschain  9429  indexfi  9430  marypha1lem  9502  eqsup  9525  supmax  9536  fisup2g  9537  fisupcl  9538  supisoex  9543  infmin  9563  fiinfg  9568  fiinf2g  9569  wofib  9614  wemaplem2  9616  card2inf  9624  brwdom2  9642  cnfcom3clem  9774  ssttrcl  9784  ttrcltr  9785  trcl  9797  frmin  9818  r1ordg  9847  r1pwss  9853  tz9.12lem3  9858  tz9.12  9859  r1elwf  9865  tcrank  9953  scottex  9954  scott0  9955  isnumi  10015  onsdom  10065  ondomen  10106  infpwfien  10131  cardaleph  10158  infenaleph  10160  alephfplem4  10176  alephfp2  10178  dfac2b  10200  ackbij1lem18  10305  ackbij1  10306  cflem  10314  cflemOLD  10315  cflecard  10322  cfsuc  10326  cfflb  10328  cofsmo  10338  coftr  10342  fin23lem7  10385  fin23lem11  10386  enfin2i  10390  fin23lem26  10394  isf32lem5  10426  isf34lem4  10446  isfin1-3  10455  fin1a2lem7  10475  axdc3lem4  10522  ttukeylem7  10584  iunfo  10608  ficard  10634  pwcfsdom  10652  fpwwe2lem11  10710  wunex  10808  eltsk2g  10820  grur1  10889  axgroth6  10897  inaprc  10905  nqereu  10998  archnq  11049  genpnmax  11076  ltexpri  11112  prlem936  11116  recexpr  11120  supexpr  11123  negexsr  11171  recexsrlem  11172  recexsr  11176  supsrlem  11180  axrnegex  11231  axrrecex  11232  axpre-sup  11238  1re  11290  dedekind  11453  dedekindle  11454  cnegex  11471  cnegex2  11472  recex  11922  receu  11935  fiminre2  12243  cju  12289  nn2ge  12320  nominpos  12530  zdiv  12713  btwnz  12746  uzwo  12976  ublbneg  12998  lbzbi  13001  zsupss  13002  uzsupss  13005  rpnnen1lem1  13043  rpnnen1lem3  13044  rpnnen1lem4  13045  rpnnen1lem5  13046  z2ge  13260  qbtwnre  13261  qbtwnxr  13262  xralrple  13267  xrsupsslem  13369  xrinfmsslem  13370  supxrpnf  13380  icc0  13455  uzsup  13914  expnbnd  14281  expmulnbnd  14284  hashkf  14381  hashdom  14428  iswrdi  14566  rtrclreclem1  15106  rtrclreclem2  15108  rtrclreclem3  15109  01sqrex  15298  resqrex  15299  sqrtneg  15316  abs1m  15384  rexanuz  15394  rexuz3  15397  rexuzre  15401  sqreu  15409  o1lo1  15583  climconst  15589  rlimclim1  15591  climshftlem  15620  rlimo1  15663  lo1add  15673  lo1mul  15674  lo1le  15700  isercoll  15716  serf0  15729  zsum  15766  fsum  15768  fsumcvg3  15777  mertenslem1  15932  ntrivcvgn0  15946  ntrivcvgmullem  15949  zprod  15985  fprod  15989  fprodntriv  15990  dvdsval2  16305  dvds0lem  16315  dvds1lem  16316  dvds2lem  16317  odd2np1lem  16388  odd2np1  16389  opeo  16413  omeo  16414  divalglem9  16449  gcdcllem3  16547  lcmcllem  16643  qredeu  16705  exprmfct  16751  isprm5  16754  odzcllem  16839  reumodprminv  16851  modprm0  16852  nnnn0modprm0  16853  pythagtriplem19  16880  pcprmpw2  16929  pockthi  16954  infpnlem2  16958  vdwlem2  17029  vdwlem10  17037  vdwlem13  17040  ramub1lem1  17073  cshwrepswhash1  17150  imasleval  17601  mreexexlem3d  17704  mreexexlem4d  17705  iscatd  17731  cat1  18164  poslubd  18483  fpwipodrs  18610  ismgmid2  18706  mgmidsssn0  18710  gsumval2a  18723  ismndd  18794  isgrpd2  18996  isgrpd  18998  imasgrp2  19095  mhmmnd  19104  ghmgrp  19106  gaorber  19348  orbsta  19353  cayleyth  19457  pmtrdifel  19522  pmtrdifwrdel  19527  pmtrdifwrdel2  19528  psgnunilem2  19537  psgnunilem3  19538  psgnvalii  19551  pgpfi1  19637  sylow1lem3  19642  sylow1lem5  19644  pgpfi  19647  sylow2alem2  19660  efgredeu  19794  lt6abl  19937  pgpfac1lem3a  20120  pgpfac1lem3  20121  pgpfac1lem5  20123  pgpfaclem1  20125  pgpfaclem3  20127  ablfaclem2  20130  dvdsrmul  20390  dvdsr01  20397  irredrmul  20453  rhmdvdsr  20534  lspf  20995  lspval  20996  lssats2  21021  lspfixed  21153  lspsolvlem  21167  zringlpir  21501  pzriprnglem13  21527  zncyg  21590  cygth  21613  frlmup4  21844  aspval  21916  evlseu  22130  fiinbas  22980  topbas  23000  pptbas  23036  clsval  23066  elcls  23102  neiint  23133  neips  23142  opnneissb  23143  opnssneib  23144  innei  23154  neiptopnei  23161  restbas  23187  neitr  23209  pnfnei  23249  mnfnei  23250  lmconst  23290  iscnp4  23292  cncnpi  23307  cnconst2  23312  cnprest  23318  cnpdis  23322  nrmsep  23386  regsep2  23405  cmpcovf  23420  cmpsub  23429  cmpcld  23431  hauscmplem  23435  conncompid  23460  2ndci  23477  2ndcsb  23478  2ndc1stc  23480  1stcrest  23482  2ndcctbss  23484  2ndcdisj  23485  2ndcomap  23487  2ndcsep  23488  dis2ndc  23489  restlly  23512  islly2  23513  hausllycmp  23523  cldllycmp  23524  lly1stc  23525  dislly  23526  ssref  23541  refref  23542  finlocfin  23549  dissnlocfin  23558  locfindis  23559  llycmpkgen2  23579  cmpkgen  23580  1stckgenlem  23582  elptr  23602  ptbasfi  23610  neitx  23636  ptpjopn  23641  txcnp  23649  ptcnplem  23650  txlly  23665  txnlly  23666  txtube  23669  txcmplem1  23670  tx1stc  23679  txkgen  23681  xkococnlem  23688  txconn  23718  tgqtop  23741  kqreglem1  23770  kqreglem2  23771  kqnrmlem1  23772  kqnrmlem2  23773  reghmph  23822  nrmhmph  23823  fbssfi  23866  opnfbas  23871  isfil2  23885  fsubbas  23896  ssfg  23901  fgss2  23903  fbasrn  23913  filuni  23914  fgtr  23919  ssufl  23947  uffix  23950  elfm2  23977  elfm3  23979  imaelfm  23980  rnelfmlem  23981  rnelfm  23982  fmfnfmlem4  23986  fmfnfm  23987  fmco  23990  ufldom  23991  hausflim  24010  flimcls  24014  hauspwpwf1  24016  flffbas  24024  txflf  24035  fclscf  24054  fclsfnflim  24056  alexsubALTlem4  24079  alexsubALT  24080  tmdgsum2  24125  symgtgp  24135  subgntr  24136  opnsubg  24137  ghmcnp  24144  qustgpopn  24149  tsmsfbas  24157  tsmsxplem1  24182  ustexsym  24245  trust  24259  utoptop  24264  restutop  24267  restutopopn  24268  ustuqtop4  24274  utopsnneiplem  24277  iducn  24313  fmucnd  24322  cfilufg  24323  trcfilu  24324  neipcfilu  24326  imasdsf1olem  24404  blssps  24455  blss  24456  blssexps  24457  blssex  24458  ssblex  24459  blin2  24460  neibl  24535  blcld  24539  metss2  24546  stdbdmopn  24552  met1stc  24555  met2ndci  24556  metrest  24558  prdsxmslem2  24563  metcnp3  24574  metustexhalf  24590  metustfbas  24591  cfilucfil  24593  restmetu  24604  dscopn  24607  ngptgp  24670  nlmvscnlem1  24728  tgioo  24837  tgqioo  24841  xrsmopn  24853  zcld  24854  recld2  24855  zdis  24857  icccmplem1  24863  icccmplem2  24864  xmetdcn2  24878  addcnlem  24905  xrhmeo  24996  cnheibor  25006  cnllycmp  25007  lebnumlem3  25014  lebnum  25015  xlebnum  25016  lebnumii  25017  elpi1i  25098  ipcnlem1  25298  lmnn  25316  iscfil3  25326  cfilres  25349  flimcfil  25367  bcthlem4  25380  bcthlem5  25381  minveclem4c  25478  minveclem2  25479  minveclem3b  25481  minveclem3  25482  minveclem4  25485  minveclem6  25487  ivthlem2  25506  ivth  25508  ivthle  25510  ivthle2  25511  elovolmr  25530  ovolunlem1  25551  ovoliunlem2  25557  ovolicc1  25570  iundisj  25602  iunmbl2  25611  dyadmbllem  25653  volivth  25661  mbflimsup  25720  i1faddlem  25747  i1fmullem  25748  itg2lr  25785  itg2monolem1  25805  limcnlp  25933  ellimc3  25934  limcflf  25936  limciun  25949  rollelem  26047  c1lip1  26056  lhop1lem  26072  ply1divex  26196  ig1peu  26234  elply2  26255  coeeq  26286  plydivlem3  26355  plydivlem4  26356  elqaalem3  26381  qaa  26383  iaa  26385  aareccl  26386  aannenlem2  26389  aalioulem2  26393  aalioulem3  26394  aalioulem5  26396  aalioulem6  26397  aaliou  26398  aaliou2  26400  aaliou3lem8  26405  ulmshftlem  26450  reeff1o  26509  pilem2  26514  pilem3  26515  efif1olem2  26603  efopn  26718  cxpcn3lem  26808  cxpeq  26818  dcubic2  26905  quart  26922  xrlimcnp  27029  ftalem5  27138  ftalem7  27140  sgmnncl  27208  dvdsppwf1o  27247  musum  27252  perfect  27293  dchrptlem1  27326  dchrptlem2  27327  dchrpt  27329  bpos1lem  27344  lgsqrlem4  27411  lgsdchrval  27416  2sqblem  27493  dchrisumlem3  27553  chpdifbndlem2  27616  pntrsumbnd2  27629  pntpbnd1  27648  pntpbnd2  27649  pntpbnd  27650  pntibndlem2  27653  pntibndlem3  27654  pntleme  27670  pntlem3  27671  elno2  27717  sltval2  27719  noreson  27723  sltres  27725  noseponlem  27727  nolesgn2o  27734  nogesgn1o  27736  nodense  27755  nosupfv  27769  nosupres  27770  nosupbnd1lem3  27773  nosupbnd1lem5  27775  nosupbnd2lem1  27778  noinffv  27784  noinfres  27785  noinfbnd1lem3  27788  noinfbnd1lem5  27790  noinfbnd2lem1  27793  noetasuplem4  27799  noetainflem4  27803  noetalem2  27805  cuteq0  27895  cuteq1  27896  oldlim  27943  cofcutrtime  27979  cofss  27982  coiniss  27983  cutlt  27984  cutmax  27986  cutmin  27987  negsex  28093  negsfo  28103  norecdiv  28234  divs1  28247  precsexlem11  28259  precsex  28260  recsex  28261  elons2d  28300  n0ons  28357  dfnns2  28380  nohalf  28425  0reno  28447  readdscl  28449  axtgcont  28495  tgcgrxfr  28544  legid  28613  btwnleg  28614  leg0  28618  tghilberti1  28663  tglnpt2  28667  colline  28675  mirreu3  28680  isperp2  28741  colperpex  28759  lnopp2hpgb  28789  hpgerlem  28791  brbtwn  28932  brcgr  28933  brbtwn2  28938  axpasch  28974  axlowdimlem14  28988  axlowdim2  28993  axcontlem2  28998  axcontlem4  29000  axcontlem8  29004  axcontlem10  29006  axcontlem12  29008  fusgrn0degnn0  29535  friendshipgt3  30430  lpni  30512  isgrpoi  30530  vacn  30726  smcnlem  30729  nmosetn0  30797  nmoolb  30803  nmobndi  30807  nmoo0  30823  nmlno0lem  30825  isblo3i  30833  blo3i  30834  blocnilem  30836  ubthlem1  30902  minvecolem2  30907  minvecolem3  30908  minvecolem4c  30911  minvecolem4  30912  minvecolem5  30913  minvecolem6  30914  norm1exi  31282  occl  31336  spanval  31365  spancl  31368  shsval2i  31419  ococin  31440  pjoml6i  31621  nmopsetn0  31897  nmfnsetn0  31910  nmoplb  31939  nmfnlb  31956  nmop0  32018  nmfn0  32019  nmlnop0iALT  32027  nmopun  32046  nmcexi  32058  lnconi  32065  lnopcnbd  32068  lnfncnbd  32089  riesz3i  32094  riesz1  32097  cnlnadjlem2  32100  cnlnadjlem8  32106  cnlnadjlem9  32107  adjbd1o  32117  branmfn  32137  opsqrlem1  32172  pjnmopi  32180  strlem1  32282  stri  32289  hstri  32297  cvcon3  32316  cvnbtwn  32318  superpos  32386  shatomici  32390  atcvat4i  32429  mdsymlem2  32436  cdj1i  32465  cdj3i  32473  rexunirn  32520  foresf1o  32532  iundisjf  32611  aciunf1lem  32680  fnpreimac  32689  fgreu  32690  fcnvgreu  32691  xrge0infss  32767  ssnnssfz  32792  iundisjfi  32801  xreceu  32886  rexdiv  32890  isarchi3  33167  archirngz  33169  archiabllem2a  33174  0nellinds  33363  qtophaus  33782  reff  33785  locfinreflem  33786  cmpcref  33796  dispcmp  33805  tpr2rico  33858  pnfneige0  33897  qqhucn  33938  rrhre  33967  indf1ofs  33990  esumcst  34027  esumpcvgval  34042  dmsigagen  34108  rossros  34144  dya2icoseg  34242  dya2iocnrect  34246  dya2iocuni  34248  eulerpartlemgvv  34341  dstfrvunirn  34439  ballotlem4  34463  ballotlemic  34471  ballotlem1c  34472  ballotlemrc  34495  signsw0g  34533  signswmnd  34534  prodfzo03  34580  tgoldbachgt  34640  loop1cycl  35105  umgr2cycllem  35108  umgr2cycl  35109  subfacp1lem3  35150  erdsze2lem2  35172  cnpconn  35198  txpconn  35200  ptpconn  35201  indispconn  35202  connpconn  35203  cvxpconn  35210  cnllysconn  35213  cvmsss2  35242  cvmcov2  35243  cvmopnlem  35246  cvmliftlem14  35265  cvmliftlem15  35266  cvmlift2lem11  35281  cvmlift2lem12  35282  cvmlift2lem13  35283  cvmlift3lem2  35288  cvmlift3lem6  35292  cvmlift3lem9  35295  mthmi  35545  r1peuqusdeg1  35611  br8  35718  br6  35719  br4  35720  dfon2lem9  35755  wzel  35788  wsuclem  35789  wsuclb  35792  imagesset  35917  fvtransport  35996  brcolinear  36023  brsegle  36072  seglerflx  36076  seglemin  36077  btwnsegle  36081  fvray  36105  fvline  36108  hilbert1.1  36118  elhf2  36139  0hf  36141  nn0prpwlem  36288  nn0prpw  36289  fness  36315  fneref  36316  fnessref  36323  refssfne  36324  neibastop2lem  36326  fnemeet1  36332  tailfb  36343  filnetlem4  36347  limsucncmpi  36411  taupilemrplb  37286  relowlssretop  37329  rdgellim  37342  matunitlindflem2  37577  ptrecube  37580  poimirlem4  37584  poimirlem17  37597  poimirlem20  37600  poimirlem23  37603  poimirlem24  37604  poimirlem26  37606  poimirlem27  37607  poimirlem29  37609  poimirlem32  37612  heicant  37615  mblfinlem1  37617  mblfinlem2  37618  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  volsupnfl  37625  itg2addnclem  37631  itg2addnclem3  37633  itg2addnc  37634  ftc1anclem5  37657  unirep  37674  cover2  37675  indexa  37693  frinfm  37695  sdclem1  37703  fdc  37705  incsequz  37708  caushft  37721  istotbnd3  37731  0totbnd  37733  sstotbnd2  37734  sstotbnd  37735  sstotbnd3  37736  isbnd3  37744  ssbnd  37748  equivbnd  37750  prdsbnd  37753  prdstotbnd  37754  cntotbnd  37756  heibor1lem  37769  heiborlem1  37771  heiborlem3  37773  heiborlem6  37776  heiborlem8  37778  bfplem2  37783  rrncmslem  37792  iccbnd  37800  opidonOLD  37812  exidres  37838  isrngod  37858  isgrpda  37915  isdrngo2  37918  igenval  38021  igenidl  38023  prtlem10  38821  lshpnel2N  38941  lsmsat  38964  lssatomic  38967  lcvnbtwn  38981  lfl1  39026  eqlkr  39055  lshpkrlem1  39066  lshpkrex  39074  cvrcon3b  39233  cvrat4  39400  3dim3  39426  ps-2  39435  llni  39465  llnle  39475  lplni  39489  lplnle  39497  lplnexllnN  39521  lvoli  39532  lnatexN  39736  elpaddn0  39757  pclfinN  39857  lhprelat3N  39997  4atexlemex2  40028  4atex  40033  4atex2-0aOLDN  40035  4atex2-0cOLDN  40037  lautcvr  40049  cdleme0ex1N  40180  cdleme50rnlem  40501  cdleme50ex  40516  cdlemg1cex  40545  cdlemkid5  40892  cdlemk  40931  tendoex  40932  cdleml5N  40937  cdlemm10N  41075  dih1dimatlem0  41285  dihjat1lem  41385  dvh3dim2  41405  dvh3dim3N  41406  dochkr1  41435  dochkr1OLDN  41436  lcfrvalsnN  41498  lcfrlem27  41526  lcfrlem37  41536  lcfr  41542  mapd1o  41605  mapdpglem23  41651  hdmap11lem2  41799  primrootsunit1  42054  zdivgd  42324  resubeu  42353  fidomncyc  42490  nacsfix  42668  mzpcompact2lem  42707  eldioph  42714  diophrw  42715  diophin  42728  rexrabdioph  42750  rexzrexnn0  42760  eldioph4b  42767  rencldnfilem  42776  irrapxlem5  42782  irrapxlem6  42783  pell1234qrdich  42817  pell14qrdich  42825  infmrgelbi  42834  pellqrex  42835  pellfundre  42837  pellfundlb  42840  rmxynorm  42875  congrep  42930  acongrep  42937  jm2.27  42965  fnwe2lem2  43008  islssfgi  43029  hbtlem2  43081  hbtlem4  43083  hbtlem5  43085  dgraaub  43105  mpaaeu  43107  aaitgo  43119  rgspnval  43125  rgspncl  43126  unielss  43179  onexgt  43201  onexomgt  43202  onexlimgt  43204  onexoegt  43205  oaordnr  43258  omnord1  43267  oenord1  43278  oaomoencom  43279  oenass  43281  tfsconcatfv2  43302  tfsconcatrn  43304  tfsconcatb0  43306  ofoafo  43318  naddcnffo  43326  oaun3lem1  43336  naddwordnexlem4  43363  sucomisnotcard  43506  clsk1independent  44008  restuni3  45020  iinssd  45033  founiiun  45086  wessf1ornlem  45092  founiiun0  45097  unirnmap  45115  dstregt0  45196  uzfissfz  45241  rpgtrecnn  45295  rexabslelem  45333  infrnmptle  45338  infxrunb3rnmpt  45343  infxrpnf  45361  supminfxr  45379  rexanuz2nf  45408  iooiinicc  45460  iooiinioc  45474  uzubioo  45485  climsuse  45529  islptre  45540  limsuppnfdlem  45622  climinf3  45637  limsupmnfuzlem  45647  limsupre3lem  45653  limsupre3uzlem  45656  0cnv  45663  liminfreuzlem  45723  cnrefiisplem  45750  icccncfext  45808  cncficcgt0  45809  dvbdfbdioo  45851  ioodvbdlimc1lem1  45852  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  stoweidlem9  45930  stoweidlem14  45935  stoweidlem18  45939  stoweidlem21  45942  stoweidlem29  45950  stoweidlem34  45955  stoweidlem35  45956  stoweidlem39  45960  stoweidlem41  45962  stoweidlem45  45966  stoweidlem52  45973  stoweidlem55  45976  stoweidlem57  45978  stoweidlem60  45981  stirlinglem5  45999  stirlinglem13  46007  stirlinglem14  46008  fourierdlem16  46044  fourierdlem20  46048  fourierdlem21  46049  fourierdlem22  46050  fourierdlem25  46053  fourierdlem31  46059  fourierdlem39  46067  fourierdlem41  46069  fourierdlem42  46070  fourierdlem47  46074  fourierdlem48  46075  fourierdlem49  46076  fourierdlem51  46078  fourierdlem63  46090  fourierdlem64  46091  fourierdlem65  46092  fourierdlem77  46104  fourierdlem81  46108  fourierdlem83  46110  fourierdlem103  46130  fourierdlem104  46131  elaa2lem  46154  etransclem47  46202  qndenserrnbl  46216  ioorrnopnlem  46225  ioorrnopnxrlem  46227  intsaluni  46250  salgencntex  46264  subsaliuncllem  46278  sge0resplit  46327  sge0seq  46367  sge0reuz  46368  nnfoctbdjlem  46376  meaiininclem  46407  hoicvrrex  46477  ovnlecvr  46479  ovnlerp  46483  hoidmv1lelem2  46513  hoidmvlelem2  46517  hoidmvlelem3  46518  ovnhoilem1  46522  ovnlecvr2  46531  hoiqssbl  46546  ovolval4lem2  46571  ovolval5lem2  46574  ovnovollem1  46577  ovnovollem2  46578  iinhoiicclem  46594  smfinflem  46738  smflimsuplem7  46747  sprsymrelfolem2  47367  perfectALTV  47597  9gbo  47648  11gbo  47649  nnsum3primes4  47662  nnsum3primesprm  47664  ssnn0ssfz  48074  lincsumcl  48160  lincscmcl  48161  zlmodzxzldep  48233  ldepsnlinc  48237  line2ylem  48485  line2xlem  48487  sepfsepc  48607  lubsscl  48640  glbsscl  48641  aacllem  48895