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 ⊢ A ≠ C ∧ B ≠ C → A B C ∖ C = A B

Proof

Step Hyp Ref Expression
1 disjprsn ⊢ A ≠ C ∧ B ≠ C → A B ∩ C = ∅
2 disj3 ⊢ A B ∩ C = ∅ ↔ A B = A B ∖ C
3 1 2 sylib ⊢ A ≠ C ∧ B ≠ C → A B = A B ∖ C
4 3 eqcomd ⊢ A ≠ C ∧ B ≠ C → A B ∖ C = A B
5 difid ⊢ C ∖ C = ∅
6 5 a1i ⊢ A ≠ C ∧ B ≠ C → C ∖ C = ∅
7 4 6 uneq12d ⊢ A ≠ C ∧ B ≠ C → A B ∖ C ∪ C ∖ C = A B ∪ ∅
8 df-tp ⊢ A B C = A B ∪ C
9 8 difeq1i ⊢ A B C ∖ C = A B ∪ C ∖ C
10 difundir ⊢ A B ∪ C ∖ C = A B ∖ C ∪ C ∖ C
11 9 10 eqtr2i ⊢ A B ∖ C ∪ C ∖ C = A B C ∖ C
12 un0 ⊢ A B ∪ ∅ = A B
13 7 11 12 3eqtr3g ⊢ A ≠ C ∧ B ≠ C → A B C ∖ C = A B