Metamath Proof Explorer

Theorem reseq2i

Description: Equality inference for restrictions. (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Hypothesis reseqi.1 ⊢A=B
Assertion reseq2i ⊢C↾A=C↾B

Proof

Step Hyp Ref Expression
1 reseqi.1 ⊢A=B
2 reseq2 ⊢A=B→C↾A=C↾B
3 1 2 ax-mp ⊢C↾A=C↾B