Theorem reseq12d 5849

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

Syntax hints:   → wi 4   = wceq 1533   ↾ cres 5552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147  df-in 3943  df-opab 5122  df-xp 5556  df-res 5562

This theorem is referenced by:  f1ossf1o  6885  tfrlem3a  8007  oieq1  8970  oieq2  8971  ackbij2lem3  9657  setsvalg  16506  resfval  17156  resfval2  17157  resf2nd  17159  lubfval  17582  glbfval  17595  dpjfval  19171  psrval  20136  znval  20676  prdsdsf  22971  prdsxmet  22973  imasdsf1olem  22977  xpsxmetlem  22983  xpsmet  22986  isxms  23051  isms  23053  setsxms  23083  setsms  23084  ressxms  23129  ressms  23130  prdsxmslem2  23133  cphsscph  23848  iscms  23942  cmsss  23948  cssbn  23972  minveclem3a  24024  dvcmulf  24536  efcvx  25031  issubgr  27047  ispth  27498  clwlknf1oclwwlkn  27857  eucrct2eupth  28018  padct  30449  isrrext  31236  csbwrecsg  34602  prdsbnd2  35067  cnpwstotbnd  35069  ldualset  36255  dvmptresicc  42196  itgcoscmulx  42246  fourierdlem73  42457  sge0fodjrnlem  42691  vonval  42815  dfateq12d  43318  rngchomrnghmresALTV  44260  fdivval  44592