Theorem 0sdomg

Description: A set strictly dominates the empty set iff it is not empty. (Contributed by NM, 23-Mar-2006)

	Ref	Expression
Assertion	0sdomg	$$⊢A\in V\to \left(\varnothing \prec A\leftrightarrow A\ne \varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		0domg	$$⊢A\in V\to \varnothing \preccurlyeq A$$
2		brsdom	$$⊢\varnothing \prec A\leftrightarrow \left(\varnothing \preccurlyeq A\wedge \neg \varnothing \approx A\right)$$
3	2	baib	$$⊢\varnothing \preccurlyeq A\to \left(\varnothing \prec A\leftrightarrow \neg \varnothing \approx A\right)$$
4	1 3	syl	$$⊢A\in V\to \left(\varnothing \prec A\leftrightarrow \neg \varnothing \approx A\right)$$
5		ensymb	$$⊢\varnothing \approx A\leftrightarrow A\approx \varnothing$$
6		en0	$$⊢A\approx \varnothing \leftrightarrow A=\varnothing$$
7	5 6	bitri	$$⊢\varnothing \approx A\leftrightarrow A=\varnothing$$
8	7	necon3bbii	$$⊢\neg \varnothing \approx A\leftrightarrow A\ne \varnothing$$
9	4 8	bitrdi	$$⊢A\in V\to \left(\varnothing \prec A\leftrightarrow A\ne \varnothing \right)$$