Theorem reseq12d 5740

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

Syntax hints:   → wi 4   = wceq 1522   ↾ cres 5450

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-rab 3114  df-v 3439  df-in 3870  df-opab 5029  df-xp 5454  df-res 5460

This theorem is referenced by:  f1ossf1o  6758  tfrlem3a  7870  oieq1  8827  oieq2  8828  ackbij2lem3  9514  setsvalg  16346  resfval  16996  resfval2  16997  resf2nd  16999  lubfval  17422  glbfval  17435  dpjfval  18899  psrval  19835  znval  20369  prdsdsf  22665  prdsxmet  22667  imasdsf1olem  22671  xpsxmetlem  22677  xpsmet  22680  isxms  22745  isms  22747  setsxms  22777  setsms  22778  ressxms  22823  ressms  22824  prdsxmslem2  22827  cphsscph  23542  iscms  23636  cmsss  23642  cssbn  23666  minveclem3a  23718  dvcmulf  24230  efcvx  24725  issubgr  26741  ispth  27196  clwlknf1oclwwlkn  27555  eucrct2eupthOLD  27718  eucrct2eupth  27719  padct  30148  isrrext  30863  csbwrecsg  34164  prdsbnd2  34630  cnpwstotbnd  34632  ldualset  35817  dvmptresicc  41771  itgcoscmulx  41821  fourierdlem73  42032  sge0fodjrnlem  42266  vonval  42390  dfateq12d  42867  rngchomrnghmresALTV  43771  fdivval  44106