Theorem reseq12d 5981

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

Syntax hints:   → wi 4   = wceq 1570   ↾ cres 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-in 3913  df-opab 5175  df-xp 5669  df-res 5675

This theorem is referenced by:  f1ossf1o  7126  csbfrecsg  8282  tfrlem3a  8364  oieq1  9475  oieq2  9476  ackbij2lem3  10224  setsvalg  17227  resfval  17950  resfval2  17951  resf2nd  17953  lubfval  18405  glbfval  18418  dpjfval  20128  znval  21666  psrval  22046  prdsdsf  24505  prdsxmet  24507  imasdsf1olem  24511  xpsxmetlem  24517  xpsmet  24520  isxms  24585  isms  24587  setsxms  24617  setsms  24618  ressxms  24663  ressms  24664  prdsxmslem2  24667  cphsscph  25391  iscms  25485  cmsss  25491  cssbn  25515  minveclem3a  25567  dvmptresicc  26056  dvcmulf  26085  efcvx  26590  issubgr  29599  ispth  30048  clwlknf1oclwwlkn  30413  eucrct2eupth  30574  ressply1evls1  33833  isrrext  34368  prdsbnd2  38424  cnpwstotbnd  38426  ldualset  39877  itgcoscmulx  46663  fourierdlem73  46873  sge0fodjrnlem  47110  vonval  47234  dfateq12d  47840  isisubgr  48604  rngchomrnghmresALTV  49021  fdivval  49296