Metamath Proof Explorer

Theorem fnfvelrn

Description: A function's value belongs to its range. (Contributed by NM, 15-Oct-1996)

Ref Expression
Assertion fnfvelrn ⊢ F Fn A ∧ B ∈ A → F ⁡ B ∈ ran ⁡ F

Proof

Step Hyp Ref Expression
1 fvelrn ⊢ Fun ⁡ F ∧ B ∈ dom ⁡ F → F ⁡ B ∈ ran ⁡ F
2 1 funfni ⊢ F Fn A ∧ B ∈ A → F ⁡ B ∈ ran ⁡ F