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\in V\to \left({F\upharpoonright }_{\left\{X\right\}}\right)\left(X\right)=F\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		snidg	$$⊢X\in V\to X\in \left\{X\right\}$$
2	1	fvresd	$$⊢X\in V\to \left({F\upharpoonright }_{\left\{X\right\}}\right)\left(X\right)=F\left(X\right)$$