Metamath Proof Explorer

Theorem ffvelcdm

Description: A function's value belongs to its codomain. (Contributed by NM, 12-Aug-1999)

Ref Expression
Assertion ffvelcdm ⊢ F : A ⟶ B ∧ C ∈ A → F ⁡ C ∈ B

Proof

Step Hyp Ref Expression
1 ffn ⊢ F : A ⟶ B → F Fn A
2 fnfvelrn ⊢ F Fn A ∧ C ∈ A → F ⁡ C ∈ ran ⁡ F
3 1 2 sylan ⊢ F : A ⟶ B ∧ C ∈ A → F ⁡ C ∈ ran ⁡ F
4 frn ⊢ F : A ⟶ B → ran ⁡ F ⊆ B
5 4 sseld ⊢ F : A ⟶ B → F ⁡ C ∈ ran ⁡ F → F ⁡ C ∈ B
6 5 adantr ⊢ F : A ⟶ B ∧ C ∈ A → F ⁡ C ∈ ran ⁡ F → F ⁡ C ∈ B
7 3 6 mpd ⊢ F : A ⟶ B ∧ C ∈ A → F ⁡ C ∈ B