Metamath Proof Explorer


Theorem ffvelcdmd

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

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

Proof

Step Hyp Ref Expression
1 ffvelcdmd.1 φ F : A B
2 ffvelcdmd.2 φ C A
3 1 ffvelcdmda φ C A F C B
4 2 3 mpdan φ F C B