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 1541   ↾ cres 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-in 3908  df-res 5636

This theorem is referenced by:  reseq12d  5939  fun2ssres  6537  funcnvres2  6572  fresin  6703  fresaunres2  6706  offres  7927  itunifval  10326  hsmex  10342  gruima  10713  fseq1p1m1  13514  ltweuz  13884  rlimres  15481  lo1res  15482  lo1resb  15487  rlimresb  15488  o1resb  15489  bitsf1ocnv  16371  fsets  17096  setsres  17105  setscom  17107  sscres  17747  resfval2  17817  estrres  18062  symgvalstruct  19326  gsumzres  19838  gsumzsplit  19856  gsum2dlem2  19900  dpjidcl  19989  pgpfaclem1  20012  funcrngcsetc  20573  funcringcsetc  20607  rhmsubclem1  20618  pwssplit2  21012  pwssplit3  21013  znle2  21508  phssip  21613  mamures  22341  ofco2  22395  mdetunilem9  22564  mdetmul  22567  smadiadetglem1  22615  smadiadetglem2  22616  tmdgsum  24039  tsmsval2  24074  tsmsres  24088  tsmssplit  24096  imasdsf1olem  24317  tmslem  24426  sranlm  24628  cmssmscld  25306  srabn  25316  cmscsscms  25329  mbflimsup  25623  dvres  25868  dvres3a  25871  dvmptresicc  25873  dvnres  25889  cpnres  25895  dvcmul  25903  dvcmulf  25904  dvcobr  25905  dvcobrOLD  25906  dvmptres3  25916  dvmptres2  25922  dvcnvlem  25936  dvlip2  25956  ftc2ditglem  26008  itgpowd  26013  aannenlem1  26292  eff1olem  26513  resqrtcn  26715  sqrtcn  26716  rlimcnp2  26932  jensenlem2  26954  ex-res  30516  rabfodom  32580  resf1o  32809  indf1ofs  32948  tocycfvres1  33192  tocycfvres2  33193  cycpmconjvlem  33223  cycpmconjslem2  33237  cyc3conja  33239  gsumind  33426  ply1gsumz  33680  evlextv  33707  lbsdiflsp0  33783  submatres  33963  zhmnrg  34122  carsggect  34475  fibp1  34558  actfunsnf1o  34761  cvmliftlem10  35488  cvmlift2lem6  35502  cvmlift2lem12  35508  satf  35547  poimirlem3  37820  ftc1anclem8  37897  ftc2nc  37899  cocnv  37922  cnpwstotbnd  37994  drngoi  38148  aks6d1c6lem2  42421  aks6d1c6lem4  42423  eldioph2  43000  dvsconst  44567  disjf1o  45431  cncfmptss  45829  limsupresuz  45943  liminfresuz  46024  itgsinexplem1  46194  itgcoscmulx  46209  itgiccshift  46220  itgperiod  46221  dirkeritg  46342  dirkercncflem2  46344  dirkercncflem4  46346  fourierdlem16  46363  fourierdlem21  46368  fourierdlem22  46369  fourierdlem28  46375  fourierdlem42  46389  fourierdlem78  46424  fourierdlem81  46427  fourierdlem83  46429  fourierdlem84  46430  fourierdlem90  46436  fourierdlem93  46439  fourierdlem103  46449  fourierdlem104  46450  sge0resrnlem  46643  ismeannd  46707  0ome  46769  hoidmvlelem3  46837  hoidmvlelem4  46838  rhmsubcALTVlem1  48523  aacllem  50042