Theorem reseq12d 5951

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

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

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 3406  df-in 3921  df-opab 5170  df-xp 5644  df-res 5650

This theorem is referenced by:  f1ossf1o  7100  csbfrecsg  8263  tfrlem3a  8345  oieq1  9465  oieq2  9466  ackbij2lem3  10193  setsvalg  17136  resfval  17854  resfval2  17855  resf2nd  17857  lubfval  18309  glbfval  18322  dpjfval  19987  znval  21445  psrval  21824  prdsdsf  24255  prdsxmet  24257  imasdsf1olem  24261  xpsxmetlem  24267  xpsmet  24270  isxms  24335  isms  24337  setsxms  24367  setsms  24368  ressxms  24413  ressms  24414  prdsxmslem2  24417  cphsscph  25151  iscms  25245  cmsss  25251  cssbn  25275  minveclem3a  25327  dvmptresicc  25817  dvcmulf  25848  efcvx  26359  issubgr  29198  ispth  29651  clwlknf1oclwwlkn  30013  eucrct2eupth  30174  padct  32643  ressply1evls1  33534  isrrext  33990  prdsbnd2  37789  cnpwstotbnd  37791  ldualset  39118  itgcoscmulx  45967  fourierdlem73  46177  sge0fodjrnlem  46414  vonval  46538  dfateq12d  47127  isisubgr  47862  rngchomrnghmresALTV  48267  fdivval  48528