Theorem reseq1d 5933

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-in 3912  df-res 5635

This theorem is referenced by:  reseq12d  5935  fun2ssres  6531  funcnvres2  6566  fresin  6697  fresaunres2  6700  offres  7925  itunifval  10329  hsmex  10345  gruima  10715  fseq1p1m1  13519  ltweuz  13886  rlimres  15483  lo1res  15484  lo1resb  15489  rlimresb  15490  o1resb  15491  bitsf1ocnv  16373  fsets  17098  setsres  17107  setscom  17109  sscres  17748  resfval2  17818  estrres  18063  symgvalstruct  19294  gsumzres  19806  gsumzsplit  19824  gsum2dlem2  19868  dpjidcl  19957  pgpfaclem1  19980  funcrngcsetc  20543  funcringcsetc  20577  rhmsubclem1  20588  pwssplit2  20982  pwssplit3  20983  znle2  21478  phssip  21583  mamures  22300  ofco2  22354  mdetunilem9  22523  mdetmul  22526  smadiadetglem1  22574  smadiadetglem2  22575  tmdgsum  23998  tsmsval2  24033  tsmsres  24047  tsmssplit  24055  imasdsf1olem  24277  tmslem  24386  sranlm  24588  cmssmscld  25266  srabn  25276  cmscsscms  25289  mbflimsup  25583  dvres  25828  dvres3a  25831  dvmptresicc  25833  dvnres  25849  cpnres  25855  dvcmul  25863  dvcmulf  25864  dvcobr  25865  dvcobrOLD  25866  dvmptres3  25876  dvmptres2  25882  dvcnvlem  25896  dvlip2  25916  ftc2ditglem  25968  itgpowd  25973  aannenlem1  26252  eff1olem  26473  resqrtcn  26675  sqrtcn  26676  rlimcnp2  26892  jensenlem2  26914  ex-res  30403  rabfodom  32467  resf1o  32686  indf1ofs  32822  tocycfvres1  33065  tocycfvres2  33066  cycpmconjvlem  33096  cycpmconjslem2  33110  cyc3conja  33112  ply1gsumz  33540  lbsdiflsp0  33598  submatres  33772  zhmnrg  33931  carsggect  34285  fibp1  34368  actfunsnf1o  34571  cvmliftlem10  35266  cvmlift2lem6  35280  cvmlift2lem12  35286  satf  35325  poimirlem3  37602  ftc1anclem8  37679  ftc2nc  37681  cocnv  37704  cnpwstotbnd  37776  drngoi  37930  aks6d1c6lem2  42144  aks6d1c6lem4  42146  eldioph2  42735  dvsconst  44303  disjf1o  45169  cncfmptss  45569  limsupresuz  45685  liminfresuz  45766  itgsinexplem1  45936  itgcoscmulx  45951  itgiccshift  45962  itgperiod  45963  dirkeritg  46084  dirkercncflem2  46086  dirkercncflem4  46088  fourierdlem16  46105  fourierdlem21  46110  fourierdlem22  46111  fourierdlem28  46117  fourierdlem42  46131  fourierdlem78  46166  fourierdlem81  46169  fourierdlem83  46171  fourierdlem84  46172  fourierdlem90  46178  fourierdlem93  46181  fourierdlem103  46191  fourierdlem104  46192  sge0resrnlem  46385  ismeannd  46449  0ome  46511  hoidmvlelem3  46579  hoidmvlelem4  46580  rhmsubcALTVlem1  48266  aacllem  49787