Metamath Proof Explorer


Theorem reseq12i

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

Ref Expression
Hypotheses reseqi.1
|- A = B
reseqi.2
|- C = D
Assertion reseq12i
|- ( A |` C ) = ( B |` D )

Proof

Step Hyp Ref Expression
1 reseqi.1
 |-  A = B
2 reseqi.2
 |-  C = D
3 1 reseq1i
 |-  ( A |` C ) = ( B |` C )
4 2 reseq2i
 |-  ( B |` C ) = ( B |` D )
5 3 4 eqtri
 |-  ( A |` C ) = ( B |` D )