Theorem reseq12d 5947

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

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

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 3402  df-in 3910  df-opab 5163  df-xp 5638  df-res 5644

This theorem is referenced by:  f1ossf1o  7083  csbfrecsg  8236  tfrlem3a  8318  oieq1  9429  oieq2  9430  ackbij2lem3  10162  setsvalg  17105  resfval  17828  resfval2  17829  resf2nd  17831  lubfval  18283  glbfval  18296  dpjfval  19998  znval  21502  psrval  21883  prdsdsf  24323  prdsxmet  24325  imasdsf1olem  24329  xpsxmetlem  24335  xpsmet  24338  isxms  24403  isms  24405  setsxms  24435  setsms  24436  ressxms  24481  ressms  24482  prdsxmslem2  24485  cphsscph  25219  iscms  25313  cmsss  25319  cssbn  25343  minveclem3a  25395  dvmptresicc  25885  dvcmulf  25916  efcvx  26427  issubgr  29356  ispth  29806  clwlknf1oclwwlkn  30171  eucrct2eupth  30332  padct  32807  ressply1evls1  33657  isrrext  34177  prdsbnd2  38035  cnpwstotbnd  38037  ldualset  39490  itgcoscmulx  46316  fourierdlem73  46526  sge0fodjrnlem  46763  vonval  46887  dfateq12d  47475  isisubgr  48211  rngchomrnghmresALTV  48628  fdivval  48888