Theorem dmressnsn

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

	Ref	Expression
Assertion	dmressnsn	$$⊢A\in \mathrm{dom}F\to \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)=\left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dmres	$$⊢\mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)=\left\{A\right\}\cap \mathrm{dom}F$$
2		snssi	$$⊢A\in \mathrm{dom}F\to \left\{A\right\}\subseteq \mathrm{dom}F$$
3		df-ss	$$⊢\left\{A\right\}\subseteq \mathrm{dom}F\leftrightarrow \left\{A\right\}\cap \mathrm{dom}F=\left\{A\right\}$$
4	2 3	sylib	$$⊢A\in \mathrm{dom}F\to \left\{A\right\}\cap \mathrm{dom}F=\left\{A\right\}$$
5	1 4	eqtrid	$$⊢A\in \mathrm{dom}F\to \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)=\left\{A\right\}$$