Theorem fvresd

Description: The value of a restricted function, deduction version of fvres . (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypothesis	fvresd.1	|- ( ph -> A e. B )
Assertion	fvresd	|- ( ph -> ( ( F |` B ) ` A ) = ( F ` A ) )

Proof

Step	Hyp	Ref	Expression
1		fvresd.1	|- ( ph -> A e. B )
2		fvres	|- ( A e. B -> ( ( F |` B ) ` A ) = ( F ` A ) )
3	1 2	syl	|- ( ph -> ( ( F |` B ) ` A ) = ( F ` A ) )