Theorem reseq12d 5970

Description: Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.)

Hypotheses

Ref	Expression
reseqd.1	⊢ (𝜑 → 𝐴 = 𝐵)
reseqd.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
reseq12d	⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐷))

Proof of Theorem reseq12d

Step	Hyp	Ref	Expression
1		reseqd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	reseq1d 5968	. 2 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
3		reseqd.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	3	reseq2d 5969	. 2 ⊢ (𝜑 → (𝐵 ↾ 𝐶) = (𝐵 ↾ 𝐷))
5	2, 4	eqtrd 2800	1 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐷))

Syntax hints:   → wi 4   = wceq 1563   ↾ cres 5654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-in 3914  df-opab 5168  df-xp 5658  df-res 5664

This theorem is referenced by:  f1ossf1o  7114  csbfrecsg  8269  tfrlem3a  8351  oieq1  9462  oieq2  9463  ackbij2lem3  10211  setsvalg  17216  resfval  17939  resfval2  17940  resf2nd  17942  lubfval  18394  glbfval  18407  dpjfval  20118  znval  21645  psrval  22025  prdsdsf  24485  prdsxmet  24487  imasdsf1olem  24491  xpsxmetlem  24497  xpsmet  24500  isxms  24565  isms  24567  setsxms  24597  setsms  24598  ressxms  24643  ressms  24644  prdsxmslem2  24647  cphsscph  25371  iscms  25465  cmsss  25471  cssbn  25495  minveclem3a  25547  dvmptresicc  26036  dvcmulf  26065  efcvx  26570  issubgr  29530  ispth  29979  clwlknf1oclwwlkn  30344  eucrct2eupth  30505  ressply1evls1  33772  isrrext  34307  prdsbnd2  38306  cnpwstotbnd  38308  ldualset  39761  itgcoscmulx  46541  fourierdlem73  46751  sge0fodjrnlem  46988  vonval  47112  dfateq12d  47718  isisubgr  48482  rngchomrnghmresALTV  48899  fdivval  49170