Theorem reseq12d 5981

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

Syntax hints:   → wi 4   = wceq 1539   ↾ cres 5677

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-in 3954  df-opab 5210  df-xp 5681  df-res 5687

This theorem is referenced by:  f1ossf1o  7127  csbfrecsg  8271  tfrlem3a  8379  oieq1  9509  oieq2  9510  ackbij2lem3  10238  setsvalg  17103  resfval  17846  resfval2  17847  resf2nd  17849  lubfval  18307  glbfval  18320  dpjfval  19966  znval  21306  psrval  21687  prdsdsf  24093  prdsxmet  24095  imasdsf1olem  24099  xpsxmetlem  24105  xpsmet  24108  isxms  24173  isms  24175  setsxms  24207  setsms  24208  ressxms  24254  ressms  24255  prdsxmslem2  24258  cphsscph  24999  iscms  25093  cmsss  25099  cssbn  25123  minveclem3a  25175  dvmptresicc  25665  dvcmulf  25696  efcvx  26197  issubgr  28795  ispth  29247  clwlknf1oclwwlkn  29604  eucrct2eupth  29765  padct  32211  isrrext  33278  prdsbnd2  36966  cnpwstotbnd  36968  ldualset  38298  itgcoscmulx  44983  fourierdlem73  45193  sge0fodjrnlem  45430  vonval  45554  dfateq12d  46132  rngchomrnghmresALTV  46982  fdivval  47312