Theorem dmsn0el

Description: The domain of a singleton is empty if the singleton's argument contains the empty set. (Contributed by NM, 15-Dec-2008)

	Ref	Expression
Assertion	dmsn0el	$$⊢\varnothing \in A\to \mathrm{dom}\left\{A\right\}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		dmsnn0	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \mathrm{dom}\left\{A\right\}\ne \varnothing$$
2		0nelelxp	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\to \neg \varnothing \in A$$
3	1 2	sylbir	$$⊢\mathrm{dom}\left\{A\right\}\ne \varnothing \to \neg \varnothing \in A$$
4	3	necon4ai	$$⊢\varnothing \in A\to \mathrm{dom}\left\{A\right\}=\varnothing$$