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 ( 𝐴 ≠ 𝐵 → ( { 𝐴 , 𝐵 } ∖ { 𝐴 } ) = { 𝐵 } )

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 ⊢ ( 𝐴 ≠ 𝐵 → ( { 𝐴 , 𝐵 } ∖ { 𝐴 } ) = { 𝐵 } )