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		eqcom	$$⊢B=A\leftrightarrow A=B$$
3	1 2	sylnib	$$⊢\left(C\in B\wedge \neg C\in A\right)\to \neg A=B$$
4		dfpss2	$$⊢A\subset B\leftrightarrow \left(A\subseteq B\wedge \neg A=B\right)$$
5	4	baibr	$$⊢A\subseteq B\to \left(\neg A=B\leftrightarrow A\subset B\right)$$
6	3 5	imbitrid	$$⊢A\subseteq B\to \left(\left(C\in B\wedge \neg C\in A\right)\to A\subset B\right)$$