Theorem reseq12d 6000

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

Syntax hints:   → wi 4   = wceq 1536   ↾ cres 5690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-in 3969  df-opab 5210  df-xp 5694  df-res 5700

This theorem is referenced by:  f1ossf1o  7147  csbfrecsg  8307  tfrlem3a  8415  oieq1  9549  oieq2  9550  ackbij2lem3  10277  setsvalg  17199  resfval  17942  resfval2  17943  resf2nd  17945  lubfval  18407  glbfval  18420  dpjfval  20089  znval  21567  psrval  21952  prdsdsf  24392  prdsxmet  24394  imasdsf1olem  24398  xpsxmetlem  24404  xpsmet  24407  isxms  24472  isms  24474  setsxms  24506  setsms  24507  ressxms  24553  ressms  24554  prdsxmslem2  24557  cphsscph  25298  iscms  25392  cmsss  25398  cssbn  25422  minveclem3a  25474  dvmptresicc  25965  dvcmulf  25996  efcvx  26507  issubgr  29302  ispth  29755  clwlknf1oclwwlkn  30112  eucrct2eupth  30273  padct  32736  isrrext  33962  prdsbnd2  37781  cnpwstotbnd  37783  ldualset  39106  itgcoscmulx  45924  fourierdlem73  46134  sge0fodjrnlem  46371  vonval  46495  dfateq12d  47075  isisubgr  47785  rngchomrnghmresALTV  48122  fdivval  48388