Theorem dmsnn0

Description: The domain of a singleton is nonzero iff the singleton argument is an ordered pair. (Contributed by NM, 14-Dec-2008) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	dmsnn0	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \mathrm{dom}\left\{A\right\}\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2	1	eldm	$$⊢x\in \mathrm{dom}\left\{A\right\}\leftrightarrow \exists yx\left\{A\right\}y$$
3		df-br	$$⊢x\left\{A\right\}y\leftrightarrow ⟨x,y⟩\in \left\{A\right\}$$
4		opex	$$⊢⟨x,y⟩\in \mathrm{V}$$
5	4	elsn	$$⊢⟨x,y⟩\in \left\{A\right\}\leftrightarrow ⟨x,y⟩=A$$
6		eqcom	$$⊢⟨x,y⟩=A\leftrightarrow A=⟨x,y⟩$$
7	3 5 6	3bitri	$$⊢x\left\{A\right\}y\leftrightarrow A=⟨x,y⟩$$
8	7	exbii	$$⊢\exists yx\left\{A\right\}y\leftrightarrow \exists yA=⟨x,y⟩$$
9	2 8	bitr2i	$$⊢\exists yA=⟨x,y⟩\leftrightarrow x\in \mathrm{dom}\left\{A\right\}$$
10	9	exbii	$$⊢\exists x\exists yA=⟨x,y⟩\leftrightarrow \exists xx\in \mathrm{dom}\left\{A\right\}$$
11		elvv	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \exists x\exists yA=⟨x,y⟩$$
12		n0	$$⊢\mathrm{dom}\left\{A\right\}\ne \varnothing \leftrightarrow \exists xx\in \mathrm{dom}\left\{A\right\}$$
13	10 11 12	3bitr4i	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \mathrm{dom}\left\{A\right\}\ne \varnothing$$