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
|- ( ph -> F : A --> B )
Assertion ffvelcdmda
|- ( ( ph /\ C e. A ) -> ( F ` C ) e. B )

Proof

Step Hyp Ref Expression
1 ffvelcdmd.1
 |-  ( ph -> F : A --> B )
2 ffvelcdm
 |-  ( ( F : A --> B /\ C e. A ) -> ( F ` C ) e. B )
3 1 2 sylan
 |-  ( ( ph /\ C e. A ) -> ( F ` C ) e. B )