Metamath Proof Explorer

Theorem ffvelrni

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

Ref Expression
Hypothesis ffvrni.1 
|- F : A --> B
Assertion ffvelrni 
|- ( C e. A -> ( F ` C ) e. B )

Proof

Step Hyp Ref Expression
1 ffvrni.1 
 |-  F : A --> B
2 ffvelrn 
 |-  ( ( F : A --> B /\ C e. A ) -> ( F ` C ) e. B )
3 1 2 mpan 
 |-  ( C e. A -> ( F ` C ) e. B )