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

Metamath Proof Explorer

Theorem ssn0

Description: A class with a nonempty subclass is nonempty. (Contributed by NM, 17-Feb-2007)

		Ref	Expression
	Assertion	ssn0	$⊢ (A \subseteq B \land A \neq \emptyset) \to B \neq \emptyset$

Step	Hyp	Ref	Expression
1		sseq0	$⊢ (A \subseteq B \land B = \emptyset) \to A = \emptyset$
2	1	ex	$⊢ A \subseteq B \to (B = \emptyset \to A = \emptyset)$
3	2	necon3d	$⊢ A \subseteq B \to (A \neq \emptyset \to B \neq \emptyset)$
4	3	imp	$⊢ (A \subseteq B \land A \neq \emptyset) \to B \neq \emptyset$