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	$$⊢A\in \mathrm{dom}F\to A\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		snidg	$$⊢A\in \mathrm{dom}F\to A\in \left\{A\right\}$$
2		dmressnsn	$$⊢A\in \mathrm{dom}F\to \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)=\left\{A\right\}$$
3	1 2	eleqtrrd	$$⊢A\in \mathrm{dom}F\to A\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)$$