Theorem reseq12d 5964

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

Syntax hints:   → wi 4   = wceq 1559   ↾ cres 5647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-in 3911  df-opab 5162  df-xp 5651  df-res 5657

This theorem is referenced by:  f1ossf1o  7106  csbfrecsg  8260  tfrlem3a  8342  oieq1  9457  oieq2  9458  ackbij2lem3  10193  setsvalg  17185  resfval  17908  resfval2  17909  resf2nd  17911  lubfval  18363  glbfval  18376  dpjfval  20080  znval  21567  psrval  21947  prdsdsf  24407  prdsxmet  24409  imasdsf1olem  24413  xpsxmetlem  24419  xpsmet  24422  isxms  24487  isms  24489  setsxms  24519  setsms  24520  ressxms  24565  ressms  24566  prdsxmslem2  24569  cphsscph  25293  iscms  25387  cmsss  25393  cssbn  25417  minveclem3a  25469  dvmptresicc  25958  dvcmulf  25987  efcvx  26489  issubgr  29418  ispth  29867  clwlknf1oclwwlkn  30232  eucrct2eupth  30393  ressply1evls1  33722  isrrext  34258  prdsbnd2  38258  cnpwstotbnd  38260  ldualset  39713  itgcoscmulx  46507  fourierdlem73  46717  sge0fodjrnlem  46954  vonval  47078  dfateq12d  47684  isisubgr  48448  rngchomrnghmresALTV  48865  fdivval  49125