Theorem 0sdom

Description: A set strictly dominates the empty set iff it is not empty. (Contributed by NM, 29-Jul-2004)

	Ref	Expression
Hypothesis	0sdom.1	$$⊢A\in \mathrm{V}$$
Assertion	0sdom	$$⊢\varnothing \prec A\leftrightarrow A\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0sdom.1	$$⊢A\in \mathrm{V}$$
2		0sdomg	$$⊢A\in \mathrm{V}\to \left(\varnothing \prec A\leftrightarrow A\ne \varnothing \right)$$
3	1 2	ax-mp	$$⊢\varnothing \prec A\leftrightarrow A\ne \varnothing$$