Metamath Proof Explorer

Theorem resmptd

Description: Restriction of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypothesis resmptd.b φ B A
Assertion resmptd φ x A C B = x B C


Step Hyp Ref Expression
1 resmptd.b φ B A
2 resmpt B A x A C B = x B C
3 1 2 syl φ x A C B = x B C