Theorem reseq1d 5952

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

Syntax hints:   → wi 4   = wceq 1540   ↾ cres 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-in 3924  df-res 5653

This theorem is referenced by:  reseq12d  5954  fun2ssres  6564  funcnvres2  6599  fresin  6732  fresaunres2  6735  offres  7965  itunifval  10376  hsmex  10392  gruima  10762  fseq1p1m1  13566  ltweuz  13933  rlimres  15531  lo1res  15532  lo1resb  15537  rlimresb  15538  o1resb  15539  bitsf1ocnv  16421  fsets  17146  setsres  17155  setscom  17157  sscres  17792  resfval2  17862  estrres  18107  symgvalstruct  19334  gsumzres  19846  gsumzsplit  19864  gsum2dlem2  19908  dpjidcl  19997  pgpfaclem1  20020  funcrngcsetc  20556  funcringcsetc  20590  rhmsubclem1  20601  pwssplit2  20974  pwssplit3  20975  znle2  21470  phssip  21574  mamures  22291  ofco2  22345  mdetunilem9  22514  mdetmul  22517  smadiadetglem1  22565  smadiadetglem2  22566  tmdgsum  23989  tsmsval2  24024  tsmsres  24038  tsmssplit  24046  imasdsf1olem  24268  tmslem  24377  sranlm  24579  cmssmscld  25257  srabn  25267  cmscsscms  25280  mbflimsup  25574  dvres  25819  dvres3a  25822  dvmptresicc  25824  dvnres  25840  cpnres  25846  dvcmul  25854  dvcmulf  25855  dvcobr  25856  dvcobrOLD  25857  dvmptres3  25867  dvmptres2  25873  dvcnvlem  25887  dvlip2  25907  ftc2ditglem  25959  itgpowd  25964  aannenlem1  26243  eff1olem  26464  resqrtcn  26666  sqrtcn  26667  rlimcnp2  26883  jensenlem2  26905  ex-res  30377  rabfodom  32441  resf1o  32660  indf1ofs  32796  tocycfvres1  33074  tocycfvres2  33075  cycpmconjvlem  33105  cycpmconjslem2  33119  cyc3conja  33121  ply1gsumz  33571  lbsdiflsp0  33629  submatres  33803  zhmnrg  33962  carsggect  34316  fibp1  34399  actfunsnf1o  34602  cvmliftlem10  35288  cvmlift2lem6  35302  cvmlift2lem12  35308  satf  35347  poimirlem3  37624  ftc1anclem8  37701  ftc2nc  37703  cocnv  37726  cnpwstotbnd  37798  drngoi  37952  aks6d1c6lem2  42166  aks6d1c6lem4  42168  eldioph2  42757  dvsconst  44326  disjf1o  45192  cncfmptss  45592  limsupresuz  45708  liminfresuz  45789  itgsinexplem1  45959  itgcoscmulx  45974  itgiccshift  45985  itgperiod  45986  dirkeritg  46107  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem16  46128  fourierdlem21  46133  fourierdlem22  46134  fourierdlem28  46140  fourierdlem42  46154  fourierdlem78  46189  fourierdlem81  46192  fourierdlem83  46194  fourierdlem84  46195  fourierdlem90  46201  fourierdlem93  46204  fourierdlem103  46214  fourierdlem104  46215  sge0resrnlem  46408  ismeannd  46472  0ome  46534  hoidmvlelem3  46602  hoidmvlelem4  46603  rhmsubcALTVlem1  48273  aacllem  49794