Theorem eldmeldmressn

Description: An element of the domain (of a relation) is an element of the domain of the restriction (of the relation) to the singleton containing this element. (Contributed by Alexander van der Vekens, 22-Jul-2018)

	Ref	Expression
Assertion	eldmeldmressn	$$⊢X\in \mathrm{dom}F\leftrightarrow X\in \mathrm{dom}\left({F\upharpoonright }_{\left\{X\right\}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		eldmressnsn	$$⊢X\in \mathrm{dom}F\to X\in \mathrm{dom}\left({F\upharpoonright }_{\left\{X\right\}}\right)$$
2		elinel2	$$⊢X\in \left(\left\{X\right\}\cap \mathrm{dom}F\right)\to X\in \mathrm{dom}F$$
3		dmres	$$⊢\mathrm{dom}\left({F\upharpoonright }_{\left\{X\right\}}\right)=\left\{X\right\}\cap \mathrm{dom}F$$
4	2 3	eleq2s	$$⊢X\in \mathrm{dom}\left({F\upharpoonright }_{\left\{X\right\}}\right)\to X\in \mathrm{dom}F$$
5	1 4	impbii	$$⊢X\in \mathrm{dom}F\leftrightarrow X\in \mathrm{dom}\left({F\upharpoonright }_{\left\{X\right\}}\right)$$