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 e. A -> ( F ` C ) e. B )

Proof

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