Metamath Proof Explorer


Theorem ffvelcdmda

Description: A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016)

Ref Expression
Hypothesis ffvelcdmd.1 φ F : A B
Assertion ffvelcdmda φ C A F C B

Proof

Step Hyp Ref Expression
1 ffvelcdmd.1 φ F : A B
2 ffvelcdm F : A B C A F C B
3 1 2 sylan φ C A F C B