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 ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( 𝐹 '''' 𝐵 ) ∈ ran 𝐹 )

Proof

Step Hyp Ref Expression
1 afv2elrn ( ( Fun 𝐹𝐵 ∈ dom 𝐹 ) → ( 𝐹 '''' 𝐵 ) ∈ ran 𝐹 )
2 1 funfni ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( 𝐹 '''' 𝐵 ) ∈ ran 𝐹 )