This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ({F ↾}_{\{X\}}) (X) = F (X)$

Proof

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