Theorem reseq12d 5943

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

Syntax hints:   → wi 4   = wceq 1541   ↾ cres 5640

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-in 3920  df-opab 5173  df-xp 5644  df-res 5650

This theorem is referenced by:  f1ossf1o  7079  csbfrecsg  8220  tfrlem3a  8328  oieq1  9457  oieq2  9458  ackbij2lem3  10186  setsvalg  17049  resfval  17792  resfval2  17793  resf2nd  17795  lubfval  18253  glbfval  18266  dpjfval  19848  znval  20975  psrval  21354  prdsdsf  23757  prdsxmet  23759  imasdsf1olem  23763  xpsxmetlem  23769  xpsmet  23772  isxms  23837  isms  23839  setsxms  23871  setsms  23872  ressxms  23918  ressms  23919  prdsxmslem2  23922  cphsscph  24652  iscms  24746  cmsss  24752  cssbn  24776  minveclem3a  24828  dvmptresicc  25317  dvcmulf  25346  efcvx  25845  issubgr  28282  ispth  28734  clwlknf1oclwwlkn  29091  eucrct2eupth  29252  padct  31704  isrrext  32670  prdsbnd2  36327  cnpwstotbnd  36329  ldualset  37660  itgcoscmulx  44330  fourierdlem73  44540  sge0fodjrnlem  44777  vonval  44901  dfateq12d  45478  rngchomrnghmresALTV  46414  fdivval  46745