Theorem reseq12d 5940

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

Syntax hints:   → wi 4   = wceq 1542   ↾ cres 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-in 3909  df-opab 5162  df-xp 5631  df-res 5637

This theorem is referenced by:  f1ossf1o  7075  csbfrecsg  8228  tfrlem3a  8310  oieq1  9421  oieq2  9422  ackbij2lem3  10154  setsvalg  17097  resfval  17820  resfval2  17821  resf2nd  17823  lubfval  18275  glbfval  18288  dpjfval  19990  znval  21494  psrval  21875  prdsdsf  24315  prdsxmet  24317  imasdsf1olem  24321  xpsxmetlem  24327  xpsmet  24330  isxms  24395  isms  24397  setsxms  24427  setsms  24428  ressxms  24473  ressms  24474  prdsxmslem2  24477  cphsscph  25211  iscms  25305  cmsss  25311  cssbn  25335  minveclem3a  25387  dvmptresicc  25877  dvcmulf  25908  efcvx  26419  issubgr  29327  ispth  29777  clwlknf1oclwwlkn  30142  eucrct2eupth  30303  padct  32778  ressply1evls1  33627  isrrext  34138  prdsbnd2  37967  cnpwstotbnd  37969  ldualset  39422  itgcoscmulx  46249  fourierdlem73  46459  sge0fodjrnlem  46696  vonval  46820  dfateq12d  47408  isisubgr  48144  rngchomrnghmresALTV  48561  fdivval  48821