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

Metamath Proof Explorer

Theorem diftpsn3

Description: Removal of a singleton from an unordered triple. (Contributed by Alexander van der Vekens, 5-Oct-2017) (Proof shortened by JJ, 23-Jul-2021)

Ref Expression
Assertion diftpsn3 ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) = { 𝐴 , 𝐵 } )

Proof

Step Hyp Ref Expression
1 disjprsn ⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐴 , 𝐵 } ∩ { 𝐶 } ) = ∅ )
2 disj3 ⊢ ( ( { 𝐴 , 𝐵 } ∩ { 𝐶 } ) = ∅ ↔ { 𝐴 , 𝐵 } = ( { 𝐴 , 𝐵 } ∖ { 𝐶 } ) )
3 1 2 sylib ⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → { 𝐴 , 𝐵 } = ( { 𝐴 , 𝐵 } ∖ { 𝐶 } ) )
4 3 eqcomd ⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐴 , 𝐵 } ∖ { 𝐶 } ) = { 𝐴 , 𝐵 } )
5 difid ⊢ ( { 𝐶 } ∖ { 𝐶 } ) = ∅
6 5 a1i ⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐶 } ∖ { 𝐶 } ) = ∅ )
7 4 6 uneq12d ⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( ( { 𝐴 , 𝐵 } ∖ { 𝐶 } ) ∪ ( { 𝐶 } ∖ { 𝐶 } ) ) = ( { 𝐴 , 𝐵 } ∪ ∅ ) )
8 df-tp ⊢ { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )
9 8 difeq1i ⊢ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) = ( ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) ∖ { 𝐶 } )
10 difundir ⊢ ( ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) ∖ { 𝐶 } ) = ( ( { 𝐴 , 𝐵 } ∖ { 𝐶 } ) ∪ ( { 𝐶 } ∖ { 𝐶 } ) )
11 9 10 eqtr2i ⊢ ( ( { 𝐴 , 𝐵 } ∖ { 𝐶 } ) ∪ ( { 𝐶 } ∖ { 𝐶 } ) ) = ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } )
12 un0 ⊢ ( { 𝐴 , 𝐵 } ∪ ∅ ) = { 𝐴 , 𝐵 }
13 7 11 12 3eqtr3g ⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) = { 𝐴 , 𝐵 } )