Theorem pssn0

Description: A proper superset is nonempty. (Contributed by Steven Nguyen, 17-Jul-2022)

	Ref	Expression
Assertion	pssn0	$$⊢A\subset B\to B\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		npss0	$$⊢\neg A\subset \varnothing$$
2		psseq2	$$⊢B=\varnothing \to \left(A\subset B\leftrightarrow A\subset \varnothing \right)$$
3	1 2	mtbiri	$$⊢B=\varnothing \to \neg A\subset B$$
4	3	necon2ai	$$⊢A\subset B\to B\ne \varnothing$$