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

Metamath Proof Explorer

Theorem difprsn2

Description: Removal of a singleton from an unordered pair. (Contributed by Alexander van der Vekens, 5-Oct-2017)

Ref Expression
Assertion difprsn2 ⊢ A ≠ B → A B ∖ B = A

Proof

Step Hyp Ref Expression
1 prcom ⊢ A B = B A
2 1 difeq1i ⊢ A B ∖ B = B A ∖ B
3 necom ⊢ A ≠ B ↔ B ≠ A
4 difprsn1 ⊢ B ≠ A → B A ∖ B = A
5 3 4 sylbi ⊢ A ≠ B → B A ∖ B = A
6 2 5 eqtrid ⊢ A ≠ B → A B ∖ B = A