Metamath Proof Explorer


Theorem ffvelcdmi

Description: A function's value belongs to its codomain. (Contributed by NM, 6-Apr-2005)

Ref Expression
Hypothesis ffvelcdmi.1 F : A B
Assertion ffvelcdmi C A F C B

Proof

Step Hyp Ref Expression
1 ffvelcdmi.1 F : A B
2 ffvelcdm F : A B C A F C B
3 1 2 mpan C A F C B