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