Metamath Proof Explorer


Theorem ffvelcdmi

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

Ref Expression
Hypothesis ffvelcdmi.1 𝐹 : 𝐴𝐵
Assertion ffvelcdmi ( 𝐶𝐴 → ( 𝐹𝐶 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 ffvelcdmi.1 𝐹 : 𝐴𝐵
2 ffvelcdm ( ( 𝐹 : 𝐴𝐵𝐶𝐴 ) → ( 𝐹𝐶 ) ∈ 𝐵 )
3 1 2 mpan ( 𝐶𝐴 → ( 𝐹𝐶 ) ∈ 𝐵 )