Theorem reseq12d 5912

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3405  df-in 3904  df-opab 5150  df-xp 5614  df-res 5620

This theorem is referenced by:  f1ossf1o  7040  csbfrecsg  8149  tfrlem3a  8257  oieq1  9348  oieq2  9349  ackbij2lem3  10077  setsvalg  16944  resfval  17684  resfval2  17685  resf2nd  17687  lubfval  18145  glbfval  18158  dpjfval  19733  znval  20822  psrval  21201  prdsdsf  23603  prdsxmet  23605  imasdsf1olem  23609  xpsxmetlem  23615  xpsmet  23618  isxms  23683  isms  23685  setsxms  23717  setsms  23718  ressxms  23764  ressms  23765  prdsxmslem2  23768  cphsscph  24498  iscms  24592  cmsss  24598  cssbn  24622  minveclem3a  24674  dvmptresicc  25163  dvcmulf  25192  efcvx  25691  issubgr  27774  ispth  28227  clwlknf1oclwwlkn  28584  eucrct2eupth  28745  padct  31189  isrrext  32090  prdsbnd2  36025  cnpwstotbnd  36027  ldualset  37359  itgcoscmulx  43760  fourierdlem73  43970  sge0fodjrnlem  44205  vonval  44329  dfateq12d  44883  rngchomrnghmresALTV  45819  fdivval  46150