Metamath Proof Explorer

Theorem difeq

Description: Rewriting an equation with class difference, without using quantifiers. (Contributed by Thierry Arnoux, 24-Sep-2017)

Ref Expression
Assertion difeq ⊢ A ∖ B = C ↔ C ∩ B = ∅ ∧ C ∪ B = A ∪ B

Proof

Step Hyp Ref Expression
1 incom ⊢ B ∩ A ∖ B = A ∖ B ∩ B
2 disjdif ⊢ B ∩ A ∖ B = ∅
3 1 2 eqtr3i ⊢ A ∖ B ∩ B = ∅
4 ineq1 ⊢ A ∖ B = C → A ∖ B ∩ B = C ∩ B
5 3 4 syl5reqr ⊢ A ∖ B = C → C ∩ B = ∅
6 undif1 ⊢ A ∖ B ∪ B = A ∪ B
7 uneq1 ⊢ A ∖ B = C → A ∖ B ∪ B = C ∪ B
8 6 7 syl5reqr ⊢ A ∖ B = C → C ∪ B = A ∪ B
9 5 8 jca ⊢ A ∖ B = C → C ∩ B = ∅ ∧ C ∪ B = A ∪ B
10 simpl ⊢ C ∩ B = ∅ ∧ C ∪ B = A ∪ B → C ∩ B = ∅
11 disj3 ⊢ C ∩ B = ∅ ↔ C = C ∖ B
12 eqcom ⊢ C = C ∖ B ↔ C ∖ B = C
13 11 12 bitri ⊢ C ∩ B = ∅ ↔ C ∖ B = C
14 10 13 sylib ⊢ C ∩ B = ∅ ∧ C ∪ B = A ∪ B → C ∖ B = C
15 difeq1 ⊢ C ∪ B = A ∪ B → C ∪ B ∖ B = A ∪ B ∖ B
16 difun2 ⊢ C ∪ B ∖ B = C ∖ B
17 difun2 ⊢ A ∪ B ∖ B = A ∖ B
18 15 16 17 3eqtr3g ⊢ C ∪ B = A ∪ B → C ∖ B = A ∖ B
19 18 eqeq1d ⊢ C ∪ B = A ∪ B → C ∖ B = C ↔ A ∖ B = C
20 19 adantl ⊢ C ∩ B = ∅ ∧ C ∪ B = A ∪ B → C ∖ B = C ↔ A ∖ B = C
21 14 20 mpbid ⊢ C ∩ B = ∅ ∧ C ∪ B = A ∪ B → A ∖ B = C
22 9 21 impbii ⊢ A ∖ B = C ↔ C ∩ B = ∅ ∧ C ∪ B = A ∪ B