Theorem reseq1d 5962

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

Syntax hints:   → wi 4   = wceq 1559   ↾ cres 5647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-in 3911  df-res 5657

This theorem is referenced by:  reseq12d  5964  fun2ssres  6562  funcnvres2  6597  fresin  6729  fresaunres2  6732  offres  7960  itunifval  10370  hsmex  10386  gruima  10757  fseq1p1m1  13600  ltweuz  13971  rlimres  15568  lo1res  15569  lo1resb  15574  rlimresb  15575  o1resb  15576  bitsf1ocnv  16461  fsets  17188  setsres  17197  setscom  17199  sscres  17839  resfval2  17909  estrres  18154  symgvalstruct  19420  gsumzres  19932  gsumzsplit  19950  gsum2dlem2  19994  dpjidcl  20083  pgpfaclem1  20106  funcrngcsetc  20669  funcringcsetc  20703  rhmsubclem1  20714  pwssplit2  21107  pwssplit3  21108  znle2  21585  phssip  21690  mamures  22437  ofco2  22491  mdetunilem9  22660  mdetmul  22663  smadiadetglem1  22711  smadiadetglem2  22712  tmdgsum  24135  tsmsval2  24170  tsmsres  24184  tsmssplit  24192  imasdsf1olem  24413  tmslem  24522  sranlm  24724  cmssmscld  25392  srabn  25402  cmscsscms  25415  mbflimsup  25708  dvres  25953  dvres3a  25956  dvmptresicc  25958  dvnres  25973  cpnres  25979  dvcmul  25986  dvcmulf  25987  dvcobr  25988  dvmptres3  25998  dvmptres2  26004  dvcnvlem  26018  dvlip2  26037  ftc2ditglem  26087  itgpowd  26092  aannenlem1  26369  eff1olem  26590  resqrtcn  26791  sqrtcn  26792  rlimcnp2  27008  jensenlem2  27029  ex-res  30589  rabfodom  32653  padct  32870  resf1o  32882  indf1ofs  33005  tocycfvres1  33251  tocycfvres2  33252  cycpmconjvlem  33282  cycpmconjslem2  33296  cyc3conja  33298  gsumind  33492  ply1gsumz  33756  evlextv  33800  lbsdiflsp0  33884  submatres  34064  zhmnrg  34223  carsggect  34576  fibp1  34659  actfunsnf1o  34862  cvmliftlem10  35608  cvmlift2lem6  35622  cvmlift2lem12  35628  satf  35667  poimirlem3  38086  ftc1anclem8  38163  ftc2nc  38165  cocnv  38188  cnpwstotbnd  38260  drngoi  38414  aks6d1c6lem2  42752  aks6d1c6lem4  42754  eldioph2  43307  dvsconst  44870  disjf1o  45733  cncfmptss  46127  limsupresuz  46241  liminfresuz  46322  itgsinexplem1  46492  itgcoscmulx  46507  itgiccshift  46518  itgperiod  46519  dirkeritg  46640  dirkercncflem2  46642  dirkercncflem4  46644  fourierdlem16  46661  fourierdlem21  46666  fourierdlem22  46667  fourierdlem28  46673  fourierdlem42  46687  fourierdlem78  46722  fourierdlem81  46725  fourierdlem83  46727  fourierdlem84  46728  fourierdlem90  46734  fourierdlem93  46737  fourierdlem103  46747  fourierdlem104  46748  sge0resrnlem  46941  ismeannd  47005  0ome  47067  hoidmvlelem3  47135  hoidmvlelem4  47136  rhmsubcALTVlem1  48867  aacllem  50386