Theorem eldmressn

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

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

Proof

Step	Hyp	Ref	Expression
1		elin	$$⊢B\in \left(\left\{A\right\}\cap \mathrm{dom}F\right)\leftrightarrow \left(B\in \left\{A\right\}\wedge B\in \mathrm{dom}F\right)$$
2		elsni	$$⊢B\in \left\{A\right\}\to B=A$$
3	2	adantr	$$⊢\left(B\in \left\{A\right\}\wedge B\in \mathrm{dom}F\right)\to B=A$$
4	1 3	sylbi	$$⊢B\in \left(\left\{A\right\}\cap \mathrm{dom}F\right)\to B=A$$
5		dmres	$$⊢\mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)=\left\{A\right\}\cap \mathrm{dom}F$$
6	4 5	eleq2s	$$⊢B\in \mathrm{dom}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to B=A$$