Theorem reseq1d 5879

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

Syntax hints:   → wi 4   = wceq 1539   ↾ cres 5582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-in 3890  df-res 5592

This theorem is referenced by:  reseq12d  5881  fun2ssres  6463  funcnvres2  6498  fresin  6627  fresaunres2  6630  offres  7799  trpredeq1  9398  trpredeq2  9399  trpredeq3  9400  itunifval  10103  hsmex  10119  gruima  10489  fseq1p1m1  13259  ltweuz  13609  rlimres  15195  lo1res  15196  lo1resb  15201  rlimresb  15202  o1resb  15203  bitsf1ocnv  16079  fsets  16798  setsres  16807  setscom  16809  sscres  17452  resfval2  17524  estrres  17772  symgvalstruct  18919  symgvalstructOLD  18920  gsumzres  19425  gsumzsplit  19443  gsum2dlem2  19487  dpjidcl  19576  pgpfaclem1  19599  pwssplit2  20237  pwssplit3  20238  znle2  20673  phssip  20775  mamures  21449  ofco2  21508  mdetunilem9  21677  mdetmul  21680  smadiadetglem1  21728  smadiadetglem2  21729  tmdgsum  23154  tsmsval2  23189  tsmsres  23203  tsmssplit  23211  imasdsf1olem  23434  tmslem  23543  tmslemOLD  23544  sranlm  23754  cmssmscld  24419  srabn  24429  cmscsscms  24442  mbflimsup  24735  dvres  24980  dvres3a  24983  dvmptresicc  24985  dvnres  25000  cpnres  25006  dvcmul  25013  dvcmulf  25014  dvcobr  25015  dvmptres3  25025  dvmptres2  25031  dvcnvlem  25045  dvlip2  25064  ftc2ditglem  25114  itgpowd  25119  aannenlem1  25393  eff1olem  25609  resqrtcn  25807  sqrtcn  25808  rlimcnp2  26021  jensenlem2  26042  ex-res  28706  rabfodom  30752  resf1o  30967  tocycfvres1  31279  tocycfvres2  31280  cycpmconjvlem  31310  cycpmconjslem2  31324  cyc3conja  31326  lbsdiflsp0  31609  submatres  31658  zhmnrg  31817  indf1ofs  31894  carsggect  32185  fibp1  32268  actfunsnf1o  32484  cvmliftlem10  33156  cvmlift2lem6  33170  cvmlift2lem12  33176  satf  33215  poimirlem3  35707  ftc1anclem8  35784  ftc2nc  35786  cocnv  35810  cnpwstotbnd  35882  drngoi  36036  eldioph2  40500  dvsconst  41837  disjf1o  42618  cncfmptss  43018  limsupresuz  43134  liminfresuz  43215  itgsinexplem1  43385  itgcoscmulx  43400  itgiccshift  43411  itgperiod  43412  dirkeritg  43533  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem16  43554  fourierdlem21  43559  fourierdlem22  43560  fourierdlem28  43566  fourierdlem42  43580  fourierdlem78  43615  fourierdlem81  43618  fourierdlem83  43620  fourierdlem84  43621  fourierdlem90  43627  fourierdlem93  43630  fourierdlem103  43640  fourierdlem104  43641  sge0resrnlem  43831  ismeannd  43895  0ome  43957  hoidmvlelem3  44025  hoidmvlelem4  44026  funcrngcsetc  45444  funcringcsetc  45481  rhmsubclem1  45532  rhmsubcALTVlem1  45550  aacllem  46391