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