Theorem reseq1d 5937

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-in 3897  df-res 5636

This theorem is referenced by:  reseq12d  5939  fun2ssres  6537  funcnvres2  6572  fresin  6703  fresaunres2  6706  offres  7929  itunifval  10329  hsmex  10345  gruima  10716  fseq1p1m1  13543  ltweuz  13914  rlimres  15511  lo1res  15512  lo1resb  15517  rlimresb  15518  o1resb  15519  bitsf1ocnv  16404  fsets  17130  setsres  17139  setscom  17141  sscres  17781  resfval2  17851  estrres  18096  symgvalstruct  19363  gsumzres  19875  gsumzsplit  19893  gsum2dlem2  19937  dpjidcl  20026  pgpfaclem1  20049  funcrngcsetc  20608  funcringcsetc  20642  rhmsubclem1  20653  pwssplit2  21047  pwssplit3  21048  znle2  21543  phssip  21648  mamures  22372  ofco2  22426  mdetunilem9  22595  mdetmul  22598  smadiadetglem1  22646  smadiadetglem2  22647  tmdgsum  24070  tsmsval2  24105  tsmsres  24119  tsmssplit  24127  imasdsf1olem  24348  tmslem  24457  sranlm  24659  cmssmscld  25327  srabn  25337  cmscsscms  25350  mbflimsup  25643  dvres  25888  dvres3a  25891  dvmptresicc  25893  dvnres  25908  cpnres  25914  dvcmul  25921  dvcmulf  25922  dvcobr  25923  dvmptres3  25933  dvmptres2  25939  dvcnvlem  25953  dvlip2  25972  ftc2ditglem  26022  itgpowd  26027  aannenlem1  26305  eff1olem  26525  resqrtcn  26726  sqrtcn  26727  rlimcnp2  26943  jensenlem2  26965  ex-res  30526  rabfodom  32590  padct  32806  resf1o  32818  indf1ofs  32941  tocycfvres1  33186  tocycfvres2  33187  cycpmconjvlem  33217  cycpmconjslem2  33231  cyc3conja  33233  gsumind  33420  ply1gsumz  33674  evlextv  33701  lbsdiflsp0  33786  submatres  33966  zhmnrg  34125  carsggect  34478  fibp1  34561  actfunsnf1o  34764  cvmliftlem10  35492  cvmlift2lem6  35506  cvmlift2lem12  35512  satf  35551  poimirlem3  37958  ftc1anclem8  38035  ftc2nc  38037  cocnv  38060  cnpwstotbnd  38132  drngoi  38286  aks6d1c6lem2  42624  aks6d1c6lem4  42626  eldioph2  43208  dvsconst  44775  disjf1o  45639  cncfmptss  46035  limsupresuz  46149  liminfresuz  46230  itgsinexplem1  46400  itgcoscmulx  46415  itgiccshift  46426  itgperiod  46427  dirkeritg  46548  dirkercncflem2  46550  dirkercncflem4  46552  fourierdlem16  46569  fourierdlem21  46574  fourierdlem22  46575  fourierdlem28  46581  fourierdlem42  46595  fourierdlem78  46630  fourierdlem81  46633  fourierdlem83  46635  fourierdlem84  46636  fourierdlem90  46642  fourierdlem93  46645  fourierdlem103  46655  fourierdlem104  46656  sge0resrnlem  46849  ismeannd  46913  0ome  46975  hoidmvlelem3  47043  hoidmvlelem4  47044  rhmsubcALTVlem1  48769  aacllem  50288