Theorem reseq12i 5968

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

This proof depends on syntax axioms:   = wceq 1570   ↾ cres 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-in 3906  df-opab 5168  df-xp 5657  df-res 5663

This theorem is used by:  cnvresid  6611  fprlem1  8302  dfoi  9489  frrlem15  9745  lubfval  18502  glbfval  18515  odulub  18559  oduglb  18561  dvlog  26961  dvlog2  26963  issubgr  29834  finsumvtxdg2size  30113  sitgclg  34957  fourierdlem57  47117  fourierdlem74  47134  fourierdlem75  47135