Theorem reseq12d 5931

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 5929	. 2 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
3		reseqd.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	3	reseq2d 5930	. 2 ⊢ (𝜑 → (𝐵 ↾ 𝐶) = (𝐵 ↾ 𝐷))
5	2, 4	eqtrd 2764	1 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐷))

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

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-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-in 3910  df-opab 5155  df-xp 5625  df-res 5631

This theorem is referenced by:  f1ossf1o  7062  csbfrecsg  8217  tfrlem3a  8299  oieq1  9404  oieq2  9405  ackbij2lem3  10134  setsvalg  17077  resfval  17799  resfval2  17800  resf2nd  17802  lubfval  18254  glbfval  18267  dpjfval  19936  znval  21442  psrval  21822  prdsdsf  24253  prdsxmet  24255  imasdsf1olem  24259  xpsxmetlem  24265  xpsmet  24268  isxms  24333  isms  24335  setsxms  24365  setsms  24366  ressxms  24411  ressms  24412  prdsxmslem2  24415  cphsscph  25149  iscms  25243  cmsss  25249  cssbn  25273  minveclem3a  25325  dvmptresicc  25815  dvcmulf  25846  efcvx  26357  issubgr  29216  ispth  29666  clwlknf1oclwwlkn  30028  eucrct2eupth  30189  padct  32663  ressply1evls1  33501  isrrext  33973  prdsbnd2  37785  cnpwstotbnd  37787  ldualset  39114  itgcoscmulx  45960  fourierdlem73  46170  sge0fodjrnlem  46407  vonval  46531  dfateq12d  47120  isisubgr  47856  rngchomrnghmresALTV  48273  fdivval  48534