Theorem reseq12d 5881

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

Syntax hints:   → wi 4   = wceq 1539   ↾ cres 5582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-in 3890  df-opab 5133  df-xp 5586  df-res 5592

This theorem is referenced by:  f1ossf1o  6982  csbfrecsg  8071  tfrlem3a  8179  oieq1  9201  oieq2  9202  ackbij2lem3  9928  setsvalg  16795  resfval  17523  resfval2  17524  resf2nd  17526  lubfval  17983  glbfval  17996  dpjfval  19573  znval  20651  psrval  21028  prdsdsf  23428  prdsxmet  23430  imasdsf1olem  23434  xpsxmetlem  23440  xpsmet  23443  isxms  23508  isms  23510  setsxms  23540  setsms  23541  ressxms  23587  ressms  23588  prdsxmslem2  23591  cphsscph  24320  iscms  24414  cmsss  24420  cssbn  24444  minveclem3a  24496  dvmptresicc  24985  dvcmulf  25014  efcvx  25513  issubgr  27541  ispth  27992  clwlknf1oclwwlkn  28349  eucrct2eupth  28510  padct  30956  isrrext  31850  prdsbnd2  35880  cnpwstotbnd  35882  ldualset  37066  itgcoscmulx  43400  fourierdlem73  43610  sge0fodjrnlem  43844  vonval  43968  dfateq12d  44505  rngchomrnghmresALTV  45442  fdivval  45773