Metamath Proof Explorer

Theorem fnafv2elrn

Description: An alternate function value belongs to the range of the function, analogous to fnfvelrn . (Contributed by AV, 2-Sep-2022)

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

Proof

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