Theorem reseq12d 5837

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

Syntax hints:   → wi 4   = wceq 1543   ↾ cres 5538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-in 3860  df-opab 5102  df-xp 5542  df-res 5548

This theorem is referenced by:  f1ossf1o  6921  tfrlem3a  8091  oieq1  9106  oieq2  9107  ackbij2lem3  9820  setsvalg  16694  resfval  17352  resfval2  17353  resf2nd  17355  lubfval  17810  glbfval  17823  dpjfval  19396  znval  20454  psrval  20828  prdsdsf  23219  prdsxmet  23221  imasdsf1olem  23225  xpsxmetlem  23231  xpsmet  23234  isxms  23299  isms  23301  setsxms  23331  setsms  23332  ressxms  23377  ressms  23378  prdsxmslem2  23381  cphsscph  24102  iscms  24196  cmsss  24202  cssbn  24226  minveclem3a  24278  dvmptresicc  24767  dvcmulf  24796  efcvx  25295  issubgr  27313  ispth  27764  clwlknf1oclwwlkn  28121  eucrct2eupth  28282  padct  30728  isrrext  31616  csbwrecsg  35184  prdsbnd2  35639  cnpwstotbnd  35641  ldualset  36825  itgcoscmulx  43128  fourierdlem73  43338  sge0fodjrnlem  43572  vonval  43696  dfateq12d  44233  rngchomrnghmresALTV  45170  fdivval  45501