Theorem reseq12d 5972

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-in 3938  df-opab 5187  df-xp 5665  df-res 5671

This theorem is referenced by:  f1ossf1o  7123  csbfrecsg  8288  tfrlem3a  8396  oieq1  9531  oieq2  9532  ackbij2lem3  10259  setsvalg  17190  resfval  17910  resfval2  17911  resf2nd  17913  lubfval  18365  glbfval  18378  dpjfval  20043  znval  21501  psrval  21880  prdsdsf  24311  prdsxmet  24313  imasdsf1olem  24317  xpsxmetlem  24323  xpsmet  24326  isxms  24391  isms  24393  setsxms  24423  setsms  24424  ressxms  24469  ressms  24470  prdsxmslem2  24473  cphsscph  25208  iscms  25302  cmsss  25308  cssbn  25332  minveclem3a  25384  dvmptresicc  25874  dvcmulf  25905  efcvx  26416  issubgr  29255  ispth  29708  clwlknf1oclwwlkn  30070  eucrct2eupth  30231  padct  32702  ressply1evls1  33583  isrrext  34036  prdsbnd2  37824  cnpwstotbnd  37826  ldualset  39148  itgcoscmulx  45965  fourierdlem73  46175  sge0fodjrnlem  46412  vonval  46536  dfateq12d  47122  isisubgr  47842  rngchomrnghmresALTV  48221  fdivval  48486