Metamath Proof Explorer

Theorem fnafvelrn

Description: A function's value belongs to its range, analogous to fnfvelrn . (Contributed by Alexander van der Vekens, 25-May-2017)

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

Proof

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