Metamath Proof Explorer

Theorem difn0

Description: If the difference of two sets is not empty, then the sets are not equal. (Contributed by Thierry Arnoux, 28-Feb-2017)

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

Proof

Step Hyp Ref Expression
1 eqimss 
 |-  ( A = B -> A C_ B )
2 ssdif0 
 |-  ( A C_ B <-> ( A \ B ) = (/) )
3 1 2 sylib 
 |-  ( A = B -> ( A \ B ) = (/) )
4 3 necon3i 
 |-  ( ( A \ B ) =/= (/) -> A =/= B )