Theorem difprsn1

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

	Ref	Expression
Assertion	difprsn1	⊢ ( 𝐴 ≠ 𝐵 → ( { 𝐴 , 𝐵 } ∖ { 𝐴 } ) = { 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		necom	⊢ ( 𝐵 ≠ 𝐴 ↔ 𝐴 ≠ 𝐵 )
2		df-pr	⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
3	2	equncomi	⊢ { 𝐴 , 𝐵 } = ( { 𝐵 } ∪ { 𝐴 } )
4	3	difeq1i	⊢ ( { 𝐴 , 𝐵 } ∖ { 𝐴 } ) = ( ( { 𝐵 } ∪ { 𝐴 } ) ∖ { 𝐴 } )
5		difun2	⊢ ( ( { 𝐵 } ∪ { 𝐴 } ) ∖ { 𝐴 } ) = ( { 𝐵 } ∖ { 𝐴 } )
6	4 5	eqtri	⊢ ( { 𝐴 , 𝐵 } ∖ { 𝐴 } ) = ( { 𝐵 } ∖ { 𝐴 } )
7		disjsn2	⊢ ( 𝐵 ≠ 𝐴 → ( { 𝐵 } ∩ { 𝐴 } ) = ∅ )
8		disj3	⊢ ( ( { 𝐵 } ∩ { 𝐴 } ) = ∅ ↔ { 𝐵 } = ( { 𝐵 } ∖ { 𝐴 } ) )
9	7 8	sylib	⊢ ( 𝐵 ≠ 𝐴 → { 𝐵 } = ( { 𝐵 } ∖ { 𝐴 } ) )
10	6 9	eqtr4id	⊢ ( 𝐵 ≠ 𝐴 → ( { 𝐴 , 𝐵 } ∖ { 𝐴 } ) = { 𝐵 } )
11	1 10	sylbir	⊢ ( 𝐴 ≠ 𝐵 → ( { 𝐴 , 𝐵 } ∖ { 𝐴 } ) = { 𝐵 } )