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 𝐹 )