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

Proof

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