Theorem reseq12d 5853

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

Syntax hints:   → wi 4   = wceq 1533   ↾ cres 5556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147  df-in 3942  df-opab 5128  df-xp 5560  df-res 5566

This theorem is referenced by:  f1ossf1o  6889  tfrlem3a  8012  oieq1  8975  oieq2  8976  ackbij2lem3  9662  setsvalg  16511  resfval  17161  resfval2  17162  resf2nd  17164  lubfval  17587  glbfval  17600  dpjfval  19176  psrval  20141  znval  20681  prdsdsf  22976  prdsxmet  22978  imasdsf1olem  22982  xpsxmetlem  22988  xpsmet  22991  isxms  23056  isms  23058  setsxms  23088  setsms  23089  ressxms  23134  ressms  23135  prdsxmslem2  23138  cphsscph  23853  iscms  23947  cmsss  23953  cssbn  23977  minveclem3a  24029  dvcmulf  24541  efcvx  25036  issubgr  27052  ispth  27503  clwlknf1oclwwlkn  27862  eucrct2eupth  28023  padct  30454  isrrext  31241  csbwrecsg  34607  prdsbnd2  35072  cnpwstotbnd  35074  ldualset  36260  dvmptresicc  42202  itgcoscmulx  42252  fourierdlem73  42463  sge0fodjrnlem  42697  vonval  42821  dfateq12d  43324  rngchomrnghmresALTV  44266  fdivval  44598