This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		0domg	$⊢ A \in V \to \emptyset ≼ A$
2		brsdom	$⊢ \emptyset ≺ A \leftrightarrow (\emptyset ≼ A \land \neg \emptyset \approx A)$
3	2	baib	$⊢ \emptyset ≼ A \to (\emptyset ≺ A \leftrightarrow \neg \emptyset \approx A)$
4	1 3	syl	$⊢ A \in V \to (\emptyset ≺ A \leftrightarrow \neg \emptyset \approx A)$
5		en0r	$⊢ \emptyset \approx A \leftrightarrow A = \emptyset$
6	5	necon3bbii	$⊢ \neg \emptyset \approx A \leftrightarrow A \neq \emptyset$
7	4 6	bitrdi	$⊢ A \in V \to (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$