Theorem ssn0

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

	Ref	Expression
Assertion	ssn0	$$⊢\left(A\subseteq B\wedge A\ne \varnothing \right)\to B\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		sseq0	$$⊢\left(A\subseteq B\wedge B=\varnothing \right)\to A=\varnothing$$
2	1	ex	$$⊢A\subseteq B\to \left(B=\varnothing \to A=\varnothing \right)$$
3	2	necon3d	$$⊢A\subseteq B\to \left(A\ne \varnothing \to B\ne \varnothing \right)$$
4	3	imp	$$⊢\left(A\subseteq B\wedge A\ne \varnothing \right)\to B\ne \varnothing$$