Theorem reseq12i 5940

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

Syntax hints:   = wceq 1541   ↾ cres 5640

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-in 3920  df-opab 5173  df-xp 5644  df-res 5650

This theorem is referenced by:  cnvresid  6585  fprlem1  8236  wfrlem5OLD  8264  dfoi  9456  frrlem15  9702  lubfval  18253  glbfval  18266  odulub  18310  oduglb  18312  dvlog  26043  dvlog2  26045  issubgr  28282  finsumvtxdg2size  28561  sitgclg  33031  fourierdlem57  44524  fourierdlem74  44541  fourierdlem75  44542