Theorem reseq1d 5943

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-in 3896  df-res 5643

This theorem is referenced by:  reseq12d  5945  fun2ssres  6543  funcnvres2  6578  fresin  6709  fresaunres2  6712  offres  7936  itunifval  10338  hsmex  10354  gruima  10725  fseq1p1m1  13552  ltweuz  13923  rlimres  15520  lo1res  15521  lo1resb  15526  rlimresb  15527  o1resb  15528  bitsf1ocnv  16413  fsets  17139  setsres  17148  setscom  17150  sscres  17790  resfval2  17860  estrres  18105  symgvalstruct  19372  gsumzres  19884  gsumzsplit  19902  gsum2dlem2  19946  dpjidcl  20035  pgpfaclem1  20058  funcrngcsetc  20617  funcringcsetc  20651  rhmsubclem1  20662  pwssplit2  21055  pwssplit3  21056  znle2  21533  phssip  21638  mamures  22362  ofco2  22416  mdetunilem9  22585  mdetmul  22588  smadiadetglem1  22636  smadiadetglem2  22637  tmdgsum  24060  tsmsval2  24095  tsmsres  24109  tsmssplit  24117  imasdsf1olem  24338  tmslem  24447  sranlm  24649  cmssmscld  25317  srabn  25327  cmscsscms  25340  mbflimsup  25633  dvres  25878  dvres3a  25881  dvmptresicc  25883  dvnres  25898  cpnres  25904  dvcmul  25911  dvcmulf  25912  dvcobr  25913  dvmptres3  25923  dvmptres2  25929  dvcnvlem  25943  dvlip2  25962  ftc2ditglem  26012  itgpowd  26017  aannenlem1  26294  eff1olem  26512  resqrtcn  26713  sqrtcn  26714  rlimcnp2  26930  jensenlem2  26951  ex-res  30511  rabfodom  32575  padct  32791  resf1o  32803  indf1ofs  32926  tocycfvres1  33171  tocycfvres2  33172  cycpmconjvlem  33202  cycpmconjslem2  33216  cyc3conja  33218  gsumind  33405  ply1gsumz  33659  evlextv  33686  lbsdiflsp0  33770  submatres  33950  zhmnrg  34109  carsggect  34462  fibp1  34545  actfunsnf1o  34748  cvmliftlem10  35476  cvmlift2lem6  35490  cvmlift2lem12  35496  satf  35535  poimirlem3  37944  ftc1anclem8  38021  ftc2nc  38023  cocnv  38046  cnpwstotbnd  38118  drngoi  38272  aks6d1c6lem2  42610  aks6d1c6lem4  42612  eldioph2  43194  dvsconst  44757  disjf1o  45621  cncfmptss  46017  limsupresuz  46131  liminfresuz  46212  itgsinexplem1  46382  itgcoscmulx  46397  itgiccshift  46408  itgperiod  46409  dirkeritg  46530  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem16  46551  fourierdlem21  46556  fourierdlem22  46557  fourierdlem28  46563  fourierdlem42  46577  fourierdlem78  46612  fourierdlem81  46615  fourierdlem83  46617  fourierdlem84  46618  fourierdlem90  46624  fourierdlem93  46627  fourierdlem103  46637  fourierdlem104  46638  sge0resrnlem  46831  ismeannd  46895  0ome  46957  hoidmvlelem3  47025  hoidmvlelem4  47026  rhmsubcALTVlem1  48757  aacllem  50276