Theorem reseq12i 5967

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

This proof depends on syntax axioms:   = wceq 1569   ↾ cres 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-in 4091  df-opab 5167  df-xp 5656  df-res 5662

This theorem is used by:  cnvresid  6619  fprlem1  8321  dfoi  9508  frrlem15  9764  lubfval  18527  glbfval  18540  odulub  18584  oduglb  18586  dvlog  26984  dvlog2  26986  issubgr  29857  finsumvtxdg2size  30136  sitgclg  35020  fourierdlem57  47266  fourierdlem74  47283  fourierdlem75  47284