Theorem afv2rnfveq

Description: If the alternate function value is defined, i.e., in the range of the function, the alternate function value equals the function's value. (Contributed by AV, 3-Sep-2022)

	Ref	Expression
Assertion	afv2rnfveq	|- ( ( F '''' A ) e. ran F -> ( F '''' A ) = ( F ` A ) )

Proof

Step	Hyp	Ref	Expression
1		dfatafv2rnb	|- ( F defAt A <-> ( F '''' A ) e. ran F )
2		dfatafv2eqfv	|- ( F defAt A -> ( F '''' A ) = ( F ` A ) )
3	1 2	sylbir	|- ( ( F '''' A ) e. ran F -> ( F '''' A ) = ( F ` A ) )