Metamath Proof Explorer

Theorem fssresd

Description: Restriction of a function with a subclass of its domain, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fssresd.1 φ F : A B
fssresd.2 φ C A
Assertion fssresd φ F C : C B


Step Hyp Ref Expression
1 fssresd.1 φ F : A B
2 fssresd.2 φ C A
3 fssres F : A B C A F C : C B
4 1 2 3 syl2anc φ F C : C B