Theorem reseq12i 5889

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 5887	. 2 ⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)
3		reseqi.2	. . 3 ⊢ 𝐶 = 𝐷
4	3	reseq2i 5888	. 2 ⊢ (𝐵 ↾ 𝐶) = (𝐵 ↾ 𝐷)
5	2, 4	eqtri 2766	1 ⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐷)

Syntax hints:   = wceq 1539   ↾ cres 5591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-in 3894  df-opab 5137  df-xp 5595  df-res 5601

This theorem is referenced by:  cnvresid  6513  fprlem1  8116  wfrlem5OLD  8144  dfoi  9270  frrlem15  9515  lubfval  18068  glbfval  18081  odulub  18125  oduglb  18127  dvlog  25806  dvlog2  25808  issubgr  27638  finsumvtxdg2size  27917  sitgclg  32309  fourierdlem57  43704  fourierdlem74  43721  fourierdlem75  43722