Theorem reseq1d 5965

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-in 3933  df-res 5666

This theorem is referenced by:  reseq12d  5967  fun2ssres  6581  funcnvres2  6616  fresin  6747  fresaunres2  6750  offres  7982  itunifval  10430  hsmex  10446  gruima  10816  fseq1p1m1  13615  ltweuz  13979  rlimres  15574  lo1res  15575  lo1resb  15580  rlimresb  15581  o1resb  15582  bitsf1ocnv  16463  fsets  17188  setsres  17197  setscom  17199  sscres  17836  resfval2  17906  estrres  18151  symgvalstruct  19378  gsumzres  19890  gsumzsplit  19908  gsum2dlem2  19952  dpjidcl  20041  pgpfaclem1  20064  funcrngcsetc  20600  funcringcsetc  20634  rhmsubclem1  20645  pwssplit2  21018  pwssplit3  21019  znle2  21514  phssip  21618  mamures  22335  ofco2  22389  mdetunilem9  22558  mdetmul  22561  smadiadetglem1  22609  smadiadetglem2  22610  tmdgsum  24033  tsmsval2  24068  tsmsres  24082  tsmssplit  24090  imasdsf1olem  24312  tmslem  24421  sranlm  24623  cmssmscld  25302  srabn  25312  cmscsscms  25325  mbflimsup  25619  dvres  25864  dvres3a  25867  dvmptresicc  25869  dvnres  25885  cpnres  25891  dvcmul  25899  dvcmulf  25900  dvcobr  25901  dvcobrOLD  25902  dvmptres3  25912  dvmptres2  25918  dvcnvlem  25932  dvlip2  25952  ftc2ditglem  26004  itgpowd  26009  aannenlem1  26288  eff1olem  26509  resqrtcn  26711  sqrtcn  26712  rlimcnp2  26928  jensenlem2  26950  ex-res  30422  rabfodom  32486  resf1o  32707  indf1ofs  32843  tocycfvres1  33121  tocycfvres2  33122  cycpmconjvlem  33152  cycpmconjslem2  33166  cyc3conja  33168  ply1gsumz  33608  lbsdiflsp0  33666  submatres  33837  zhmnrg  33996  carsggect  34350  fibp1  34433  actfunsnf1o  34636  cvmliftlem10  35316  cvmlift2lem6  35330  cvmlift2lem12  35336  satf  35375  poimirlem3  37647  ftc1anclem8  37724  ftc2nc  37726  cocnv  37749  cnpwstotbnd  37821  drngoi  37975  aks6d1c6lem2  42184  aks6d1c6lem4  42186  eldioph2  42785  dvsconst  44354  disjf1o  45215  cncfmptss  45616  limsupresuz  45732  liminfresuz  45813  itgsinexplem1  45983  itgcoscmulx  45998  itgiccshift  46009  itgperiod  46010  dirkeritg  46131  dirkercncflem2  46133  dirkercncflem4  46135  fourierdlem16  46152  fourierdlem21  46157  fourierdlem22  46158  fourierdlem28  46164  fourierdlem42  46178  fourierdlem78  46213  fourierdlem81  46216  fourierdlem83  46218  fourierdlem84  46219  fourierdlem90  46225  fourierdlem93  46228  fourierdlem103  46238  fourierdlem104  46239  sge0resrnlem  46432  ismeannd  46496  0ome  46558  hoidmvlelem3  46626  hoidmvlelem4  46627  rhmsubcALTVlem1  48256  aacllem  49665