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