Theorem ssnelpss

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

	Ref	Expression
Assertion	ssnelpss	|- ( A C_ B -> ( ( C e. B /\ -. C e. A ) -> A C. B ) )

Proof

Step	Hyp	Ref	Expression
1		nelneq2	|- ( ( C e. B /\ -. C e. A ) -> -. B = A )
2	1	neqcomd	|- ( ( C e. B /\ -. C e. A ) -> -. A = B )
3		dfpss2	|- ( A C. B <-> ( A C_ B /\ -. A = B ) )
4	3	baibr	|- ( A C_ B -> ( -. A = B <-> A C. B ) )
5	2 4	imbitrid	|- ( A C_ B -> ( ( C e. B /\ -. C e. A ) -> A C. B ) )