Theorem fvressn

Description: The value of a function restricted to the singleton containing the argument equals the value of the function for this argument. (Contributed by Alexander van der Vekens, 22-Jul-2018)

	Ref	Expression
Assertion	fvressn	|- ( X e. V -> ( ( F |` { X } ) ` X ) = ( F ` X ) )

Proof

Step	Hyp	Ref	Expression
1		snidg	|- ( X e. V -> X e. { X } )
2	1	fvresd	|- ( X e. V -> ( ( F |` { X } ) ` X ) = ( F ` X ) )