Theorem reseq12i 5888

Description: Equality inference for restrictions. (Contributed by NM, 21-Oct-2014.)

Hypotheses

Ref	Expression
reseqi.1	⊢ 𝐴 = 𝐵
reseqi.2	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
reseq12i	⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐷)

Proof of Theorem reseq12i

Step	Hyp	Ref	Expression
1		reseqi.1	. . 3 ⊢ 𝐴 = 𝐵
2	1	reseq1i 5886	. 2 ⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)
3		reseqi.2	. . 3 ⊢ 𝐶 = 𝐷
4	3	reseq2i 5887	. 2 ⊢ (𝐵 ↾ 𝐶) = (𝐵 ↾ 𝐷)
5	2, 4	eqtri 2768	1 ⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐷)

Syntax hints:   = wceq 1542   ↾ cres 5592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-in 3899  df-opab 5142  df-xp 5596  df-res 5602

This theorem is referenced by:  cnvresid  6511  fprlem1  8107  wfrlem5OLD  8135  dfoi  9248  frrlem15  9516  lubfval  18066  glbfval  18079  odulub  18123  oduglb  18125  dvlog  25804  dvlog2  25806  issubgr  27636  finsumvtxdg2size  27915  sitgclg  32305  fourierdlem57  43675  fourierdlem74  43692  fourierdlem75  43693