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 V F X X = F X


Step Hyp Ref Expression
1 snidg X V X X
2 1 fvresd X V F X X = F X