Theorem sdom0

Description: The empty set does not strictly dominate any set. (Contributed by NM, 26-Oct-2003) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 29-Nov-2024)

	Ref	Expression
Assertion	sdom0	$$⊢\neg A\prec \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		dom0	$$⊢A\preccurlyeq \varnothing \leftrightarrow A=\varnothing$$
2		en0	$$⊢A\approx \varnothing \leftrightarrow A=\varnothing$$
3	1 2	sylbb2	$$⊢A\preccurlyeq \varnothing \to A\approx \varnothing$$
4		iman	$$⊢\left(A\preccurlyeq \varnothing \to A\approx \varnothing \right)\leftrightarrow \neg \left(A\preccurlyeq \varnothing \wedge \neg A\approx \varnothing \right)$$
5	3 4	mpbi	$$⊢\neg \left(A\preccurlyeq \varnothing \wedge \neg A\approx \varnothing \right)$$
6		brsdom	$$⊢A\prec \varnothing \leftrightarrow \left(A\preccurlyeq \varnothing \wedge \neg A\approx \varnothing \right)$$
7	5 6	mtbir	$$⊢\neg A\prec \varnothing$$