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

Metamath Proof Explorer

Theorem difprsn1

Description: Removal of a singleton from an unordered pair. (Contributed by Thierry Arnoux, 4-Feb-2017)

Ref Expression
Assertion difprsn1 
|- ( A =/= B -> ( { A , B } \ { A } ) = { B } )

Proof

Step Hyp Ref Expression
1 necom 
 |-  ( B =/= A <-> A =/= B )
2 df-pr 
 |-  { A , B } = ( { A } u. { B } )
3 2 equncomi 
 |-  { A , B } = ( { B } u. { A } )
4 3 difeq1i 
 |-  ( { A , B } \ { A } ) = ( ( { B } u. { A } ) \ { A } )
5 difun2 
 |-  ( ( { B } u. { A } ) \ { A } ) = ( { B } \ { A } )
6 4 5 eqtri 
 |-  ( { A , B } \ { A } ) = ( { B } \ { A } )
7 disjsn2 
 |-  ( B =/= A -> ( { B } i^i { A } ) = (/) )
8 disj3 
 |-  ( ( { B } i^i { A } ) = (/) <-> { B } = ( { B } \ { A } ) )
9 7 8 sylib 
 |-  ( B =/= A -> { B } = ( { B } \ { A } ) )
10 6 9 eqtr4id 
 |-  ( B =/= A -> ( { A , B } \ { A } ) = { B } )
11 1 10 sylbir 
 |-  ( A =/= B -> ( { A , B } \ { A } ) = { B } )