Theorem difprsn2

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

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

Proof

Step	Hyp	Ref	Expression
1		prcom	⊢ { 𝐴 , 𝐵 } = { 𝐵 , 𝐴 }
2	1	difeq1i	⊢ ( { 𝐴 , 𝐵 } ∖ { 𝐵 } ) = ( { 𝐵 , 𝐴 } ∖ { 𝐵 } )
3		necom	⊢ ( 𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴 )
4		difprsn1	⊢ ( 𝐵 ≠ 𝐴 → ( { 𝐵 , 𝐴 } ∖ { 𝐵 } ) = { 𝐴 } )
5	3 4	sylbi	⊢ ( 𝐴 ≠ 𝐵 → ( { 𝐵 , 𝐴 } ∖ { 𝐵 } ) = { 𝐴 } )
6	2 5	syl5eq	⊢ ( 𝐴 ≠ 𝐵 → ( { 𝐴 , 𝐵 } ∖ { 𝐵 } ) = { 𝐴 } )