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 } )