Theorem reseq12d 5935

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

Syntax hints:   → wi 4   = wceq 1540   ↾ cres 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-in 3912  df-opab 5158  df-xp 5629  df-res 5635

This theorem is referenced by:  f1ossf1o  7066  csbfrecsg  8224  tfrlem3a  8306  oieq1  9423  oieq2  9424  ackbij2lem3  10153  setsvalg  17095  resfval  17817  resfval2  17818  resf2nd  17820  lubfval  18272  glbfval  18285  dpjfval  19954  znval  21460  psrval  21840  prdsdsf  24271  prdsxmet  24273  imasdsf1olem  24277  xpsxmetlem  24283  xpsmet  24286  isxms  24351  isms  24353  setsxms  24383  setsms  24384  ressxms  24429  ressms  24430  prdsxmslem2  24433  cphsscph  25167  iscms  25261  cmsss  25267  cssbn  25291  minveclem3a  25343  dvmptresicc  25833  dvcmulf  25864  efcvx  26375  issubgr  29234  ispth  29684  clwlknf1oclwwlkn  30046  eucrct2eupth  30207  padct  32676  ressply1evls1  33510  isrrext  33966  prdsbnd2  37774  cnpwstotbnd  37776  ldualset  39103  itgcoscmulx  45951  fourierdlem73  46161  sge0fodjrnlem  46398  vonval  46522  dfateq12d  47111  isisubgr  47846  rngchomrnghmresALTV  48251  fdivval  48512