Theorem dom0

Description: A set dominated by the empty set is empty. (Contributed by NM, 22-Nov-2004)

	Ref	Expression
Assertion	dom0	$$⊢A\preccurlyeq \varnothing \leftrightarrow A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
2	1	brrelex1i	$$⊢A\preccurlyeq \varnothing \to A\in \mathrm{V}$$
3		0domg	$$⊢A\in \mathrm{V}\to \varnothing \preccurlyeq A$$
4	2 3	syl	$$⊢A\preccurlyeq \varnothing \to \varnothing \preccurlyeq A$$
5	4	pm4.71i	$$⊢A\preccurlyeq \varnothing \leftrightarrow \left(A\preccurlyeq \varnothing \wedge \varnothing \preccurlyeq A\right)$$
6		sbthb	$$⊢\left(A\preccurlyeq \varnothing \wedge \varnothing \preccurlyeq A\right)\leftrightarrow A\approx \varnothing$$
7		en0	$$⊢A\approx \varnothing \leftrightarrow A=\varnothing$$
8	5 6 7	3bitri	$$⊢A\preccurlyeq \varnothing \leftrightarrow A=\varnothing$$