Metamath Proof Explorer

Theorem reseq2d

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

Ref Expression
Hypothesis reseqd.1 ⊢ φ → A = B
Assertion reseq2d ⊢ φ → C ↾ A = C ↾ B

Proof

Step Hyp Ref Expression
1 reseqd.1 ⊢ φ → A = B
2 reseq2 ⊢ A = B → C ↾ A = C ↾ B
3 1 2 syl ⊢ φ → C ↾ A = C ↾ B