Theorem reseq12d 5926

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

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

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 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3394  df-in 3907  df-opab 5152  df-xp 5620  df-res 5626

This theorem is referenced by:  f1ossf1o  7056  csbfrecsg  8209  tfrlem3a  8291  oieq1  9393  oieq2  9394  ackbij2lem3  10123  setsvalg  17069  resfval  17791  resfval2  17792  resf2nd  17794  lubfval  18246  glbfval  18259  dpjfval  19962  znval  21465  psrval  21845  prdsdsf  24275  prdsxmet  24277  imasdsf1olem  24281  xpsxmetlem  24287  xpsmet  24290  isxms  24355  isms  24357  setsxms  24387  setsms  24388  ressxms  24433  ressms  24434  prdsxmslem2  24437  cphsscph  25171  iscms  25265  cmsss  25271  cssbn  25295  minveclem3a  25347  dvmptresicc  25837  dvcmulf  25868  efcvx  26379  issubgr  29242  ispth  29692  clwlknf1oclwwlkn  30054  eucrct2eupth  30215  padct  32691  ressply1evls1  33518  isrrext  34003  prdsbnd2  37814  cnpwstotbnd  37816  ldualset  39143  itgcoscmulx  45986  fourierdlem73  46196  sge0fodjrnlem  46433  vonval  46557  dfateq12d  47136  isisubgr  47872  rngchomrnghmresALTV  48289  fdivval  48550