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