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