This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∖ 𝐵 ) ≠ ∅ → 𝐴 ≠ 𝐵 )

Proof

Step Hyp Ref Expression
1 eqimss ⊢ ( 𝐴 = 𝐵 → 𝐴 ⊆ 𝐵 )
2 ssdif0 ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∖ 𝐵 ) = ∅ )
3 1 2 sylib ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∖ 𝐵 ) = ∅ )
4 3 necon3i ⊢ ( ( 𝐴 ∖ 𝐵 ) ≠ ∅ → 𝐴 ≠ 𝐵 )