Metamath Proof Explorer

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 eqcom 
 |-  ( B = A <-> A = B )
3 1 2 sylnib 
 |-  ( ( C e. B /\ -. C e. A ) -> -. A = B )
4 dfpss2 
 |-  ( A C. B <-> ( A C_ B /\ -. A = B ) )
5 4 baibr 
 |-  ( A C_ B -> ( -. A = B <-> A C. B ) )
6 3 5 syl5ib 
 |-  ( A C_ B -> ( ( C e. B /\ -. C e. A ) -> A C. B ) )