This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ F : A ⟶ B
Assertion ffvelcdmi ⊢ C ∈ A → F ⁡ C ∈ B

Proof

Step Hyp Ref Expression
1 ffvelcdmi.1 ⊢ F : A ⟶ B
2 ffvelcdm ⊢ F : A ⟶ B ∧ C ∈ A → F ⁡ C ∈ B
3 1 2 mpan ⊢ C ∈ A → F ⁡ C ∈ B