Metamath Proof Explorer


Theorem eldmressnsn

Description: The element of the domain of a restriction to a singleton is the element of the singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017)

Ref Expression
Assertion eldmressnsn AdomFAdomFA

Proof

Step Hyp Ref Expression
1 snidg AdomFAA
2 dmressnsn AdomFdomFA=A
3 1 2 eleqtrrd AdomFAdomFA