Theorem afv2elrn

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

	Ref	Expression
Assertion	afv2elrn	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		fundmdfat	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → 𝐹 defAt 𝐴 )
2		dfatafv2rnb	⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 )
3	1 2	sylib	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 )