Metamath Proof Explorer

Theorem pssdifn0

Description: A proper subclass has a nonempty difference. (Contributed by NM, 3-May-1994)

Ref Expression
Assertion pssdifn0 
|- ( ( A C_ B /\ A =/= B ) -> ( B \ A ) =/= (/) )

Proof

Step Hyp Ref Expression
1 ssdif0 
 |-  ( B C_ A <-> ( B \ A ) = (/) )
2 eqss 
 |-  ( A = B <-> ( A C_ B /\ B C_ A ) )
3 2 simplbi2 
 |-  ( A C_ B -> ( B C_ A -> A = B ) )
4 1 3 syl5bir 
 |-  ( A C_ B -> ( ( B \ A ) = (/) -> A = B ) )
5 4 necon3d 
 |-  ( A C_ B -> ( A =/= B -> ( B \ A ) =/= (/) ) )
6 5 imp 
 |-  ( ( A C_ B /\ A =/= B ) -> ( B \ A ) =/= (/) )