Theorem 0sdomg

Description: A set strictly dominates the empty set iff it is not empty. (Contributed by NM, 23-Mar-2006) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 29-Nov-2024)

	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		en0r	$$⊢\varnothing \approx A\leftrightarrow A=\varnothing$$
6	5	necon3bbii	$$⊢\neg \varnothing \approx A\leftrightarrow A\ne \varnothing$$
7	4 6	bitrdi	$$⊢A\in V\to \left(\varnothing \prec A\leftrightarrow A\ne \varnothing \right)$$