Theorem pssdif

Description: A proper subclass has a nonempty difference. (Contributed by Mario Carneiro, 27-Apr-2016)

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

Proof

Step	Hyp	Ref	Expression
1		df-pss	$$⊢A\subset B\leftrightarrow \left(A\subseteq B\wedge A\ne B\right)$$
2		pssdifn0	$$⊢\left(A\subseteq B\wedge A\ne B\right)\to B\setminus A\ne \varnothing$$
3	1 2	sylbi	$$⊢A\subset B\to B\setminus A\ne \varnothing$$