Theorem ssnelpss

Description: A subclass missing a member is a proper subclass. (Contributed by NM, 12-Jan-2002)

	Ref	Expression
Assertion	ssnelpss	$$⊢A\subseteq B\to \left(\left(C\in B\wedge \neg C\in A\right)\to A\subset B\right)$$

Proof

Step	Hyp	Ref	Expression
1		nelneq2	$$⊢\left(C\in B\wedge \neg C\in A\right)\to \neg B=A$$
2	1	neqcomd	$$⊢\left(C\in B\wedge \neg C\in A\right)\to \neg A=B$$
3		dfpss2	$$⊢A\subset B\leftrightarrow \left(A\subseteq B\wedge \neg A=B\right)$$
4	3	baibr	$$⊢A\subseteq B\to \left(\neg A=B\leftrightarrow A\subset B\right)$$
5	2 4	imbitrid	$$⊢A\subseteq B\to \left(\left(C\in B\wedge \neg C\in A\right)\to A\subset B\right)$$