Theorem reseq1d 5932

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 5927	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))

Syntax hints:   → wi 4   = wceq 1542   ↾ cres 5622

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3388  df-in 3892  df-res 5632

This theorem is referenced by:  reseq12d  5934  fun2ssres  6532  funcnvres2  6567  fresin  6698  fresaunres2  6701  offres  7925  itunifval  10327  hsmex  10343  gruima  10714  fseq1p1m1  13541  ltweuz  13912  rlimres  15509  lo1res  15510  lo1resb  15515  rlimresb  15516  o1resb  15517  bitsf1ocnv  16402  fsets  17128  setsres  17137  setscom  17139  sscres  17779  resfval2  17849  estrres  18094  symgvalstruct  19361  gsumzres  19873  gsumzsplit  19891  gsum2dlem2  19935  dpjidcl  20024  pgpfaclem1  20047  funcrngcsetc  20606  funcringcsetc  20640  rhmsubclem1  20651  pwssplit2  21044  pwssplit3  21045  znle2  21522  phssip  21627  mamures  22350  ofco2  22404  mdetunilem9  22573  mdetmul  22576  smadiadetglem1  22624  smadiadetglem2  22625  tmdgsum  24048  tsmsval2  24083  tsmsres  24097  tsmssplit  24105  imasdsf1olem  24326  tmslem  24435  sranlm  24637  cmssmscld  25305  srabn  25315  cmscsscms  25328  mbflimsup  25621  dvres  25866  dvres3a  25869  dvmptresicc  25871  dvnres  25886  cpnres  25892  dvcmul  25899  dvcmulf  25900  dvcobr  25901  dvmptres3  25911  dvmptres2  25917  dvcnvlem  25931  dvlip2  25950  ftc2ditglem  26000  itgpowd  26005  aannenlem1  26282  eff1olem  26500  resqrtcn  26701  sqrtcn  26702  rlimcnp2  26918  jensenlem2  26939  ex-res  30499  rabfodom  32563  padct  32779  resf1o  32791  indf1ofs  32914  tocycfvres1  33159  tocycfvres2  33160  cycpmconjvlem  33190  cycpmconjslem2  33204  cyc3conja  33206  gsumind  33393  ply1gsumz  33647  evlextv  33674  lbsdiflsp0  33758  submatres  33938  zhmnrg  34097  carsggect  34450  fibp1  34533  actfunsnf1o  34736  cvmliftlem10  35464  cvmlift2lem6  35478  cvmlift2lem12  35484  satf  35523  poimirlem3  37932  ftc1anclem8  38009  ftc2nc  38011  cocnv  38034  cnpwstotbnd  38106  drngoi  38260  aks6d1c6lem2  42598  aks6d1c6lem4  42600  eldioph2  43182  dvsconst  44745  disjf1o  45609  cncfmptss  46005  limsupresuz  46119  liminfresuz  46200  itgsinexplem1  46370  itgcoscmulx  46385  itgiccshift  46396  itgperiod  46397  dirkeritg  46518  dirkercncflem2  46520  dirkercncflem4  46522  fourierdlem16  46539  fourierdlem21  46544  fourierdlem22  46545  fourierdlem28  46551  fourierdlem42  46565  fourierdlem78  46600  fourierdlem81  46603  fourierdlem83  46605  fourierdlem84  46606  fourierdlem90  46612  fourierdlem93  46615  fourierdlem103  46625  fourierdlem104  46626  sge0resrnlem  46819  ismeannd  46883  0ome  46945  hoidmvlelem3  47013  hoidmvlelem4  47014  rhmsubcALTVlem1  48745  aacllem  50264