Theorem reseq1d 5927

Description: Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.)

Hypothesis

Ref	Expression
reseqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
reseq1d	⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))

Proof of Theorem reseq1d

Step	Hyp	Ref	Expression
1		reseqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		reseq1 5922	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))

Syntax hints:   → wi 4   = wceq 1541   ↾ cres 5618

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-in 3909  df-res 5628

This theorem is referenced by:  reseq12d  5929  fun2ssres  6526  funcnvres2  6561  fresin  6692  fresaunres2  6695  offres  7915  itunifval  10304  hsmex  10320  gruima  10690  fseq1p1m1  13495  ltweuz  13865  rlimres  15462  lo1res  15463  lo1resb  15468  rlimresb  15469  o1resb  15470  bitsf1ocnv  16352  fsets  17077  setsres  17086  setscom  17088  sscres  17727  resfval2  17797  estrres  18042  symgvalstruct  19307  gsumzres  19819  gsumzsplit  19837  gsum2dlem2  19881  dpjidcl  19970  pgpfaclem1  19993  funcrngcsetc  20553  funcringcsetc  20587  rhmsubclem1  20598  pwssplit2  20992  pwssplit3  20993  znle2  21488  phssip  21593  mamures  22310  ofco2  22364  mdetunilem9  22533  mdetmul  22536  smadiadetglem1  22584  smadiadetglem2  22585  tmdgsum  24008  tsmsval2  24043  tsmsres  24057  tsmssplit  24065  imasdsf1olem  24286  tmslem  24395  sranlm  24597  cmssmscld  25275  srabn  25285  cmscsscms  25298  mbflimsup  25592  dvres  25837  dvres3a  25840  dvmptresicc  25842  dvnres  25858  cpnres  25864  dvcmul  25872  dvcmulf  25873  dvcobr  25874  dvcobrOLD  25875  dvmptres3  25885  dvmptres2  25891  dvcnvlem  25905  dvlip2  25925  ftc2ditglem  25977  itgpowd  25982  aannenlem1  26261  eff1olem  26482  resqrtcn  26684  sqrtcn  26685  rlimcnp2  26901  jensenlem2  26923  ex-res  30416  rabfodom  32480  resf1o  32708  indf1ofs  32842  tocycfvres1  33074  tocycfvres2  33075  cycpmconjvlem  33105  cycpmconjslem2  33119  cyc3conja  33121  gsumind  33305  ply1gsumz  33554  lbsdiflsp0  33634  submatres  33814  zhmnrg  33973  carsggect  34326  fibp1  34409  actfunsnf1o  34612  cvmliftlem10  35326  cvmlift2lem6  35340  cvmlift2lem12  35346  satf  35385  poimirlem3  37662  ftc1anclem8  37739  ftc2nc  37741  cocnv  37764  cnpwstotbnd  37836  drngoi  37990  aks6d1c6lem2  42203  aks6d1c6lem4  42205  eldioph2  42794  dvsconst  44362  disjf1o  45227  cncfmptss  45626  limsupresuz  45740  liminfresuz  45821  itgsinexplem1  45991  itgcoscmulx  46006  itgiccshift  46017  itgperiod  46018  dirkeritg  46139  dirkercncflem2  46141  dirkercncflem4  46143  fourierdlem16  46160  fourierdlem21  46165  fourierdlem22  46166  fourierdlem28  46172  fourierdlem42  46186  fourierdlem78  46221  fourierdlem81  46224  fourierdlem83  46226  fourierdlem84  46227  fourierdlem90  46233  fourierdlem93  46236  fourierdlem103  46246  fourierdlem104  46247  sge0resrnlem  46440  ismeannd  46504  0ome  46566  hoidmvlelem3  46634  hoidmvlelem4  46635  rhmsubcALTVlem1  48311  aacllem  49832