Metamath Proof Explorer

Theorem pssdif

Description: A proper subclass has a nonempty difference. (Contributed by Mario Carneiro, 27-Apr-2016)

Ref Expression
Assertion pssdif 
|- ( A C. B -> ( B \ A ) =/= (/) )

Proof

Step Hyp Ref Expression
1 df-pss 
 |-  ( A C. B <-> ( A C_ B /\ A =/= B ) )
2 pssdifn0 
 |-  ( ( A C_ B /\ A =/= B ) -> ( B \ A ) =/= (/) )
3 1 2 sylbi 
 |-  ( A C. B -> ( B \ A ) =/= (/) )