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 ineq1 ⊢ A ∖ B = C → A ∖ B ∩ B = C ∩ B
2 disjdifr ⊢ A ∖ B ∩ B = ∅
3 1 2 eqtr3di ⊢ A ∖ B = C → C ∩ B = ∅
4 uneq1 ⊢ A ∖ B = C → A ∖ B ∪ B = C ∪ B
5 undif1 ⊢ A ∖ B ∪ B = A ∪ B
6 4 5 eqtr3di ⊢ A ∖ B = C → C ∪ B = A ∪ B
7 3 6 jca ⊢ A ∖ B = C → C ∩ B = ∅ ∧ C ∪ B = A ∪ B
8 simpl ⊢ C ∩ B = ∅ ∧ C ∪ B = A ∪ B → C ∩ B = ∅
9 disj3 ⊢ C ∩ B = ∅ ↔ C = C ∖ B
10 eqcom ⊢ C = C ∖ B ↔ C ∖ B = C
11 9 10 bitri ⊢ C ∩ B = ∅ ↔ C ∖ B = C
12 8 11 sylib ⊢ C ∩ B = ∅ ∧ C ∪ B = A ∪ B → C ∖ B = C
13 difeq1 ⊢ C ∪ B = A ∪ B → C ∪ B ∖ B = A ∪ B ∖ B
14 difun2 ⊢ C ∪ B ∖ B = C ∖ B
15 difun2 ⊢ A ∪ B ∖ B = A ∖ B
16 13 14 15 3eqtr3g ⊢ C ∪ B = A ∪ B → C ∖ B = A ∖ B
17 16 eqeq1d ⊢ C ∪ B = A ∪ B → C ∖ B = C ↔ A ∖ B = C
18 17 adantl ⊢ C ∩ B = ∅ ∧ C ∪ B = A ∪ B → C ∖ B = C ↔ A ∖ B = C
19 12 18 mpbid ⊢ C ∩ B = ∅ ∧ C ∪ B = A ∪ B → A ∖ B = C
20 7 19 impbii ⊢ A ∖ B = C ↔ C ∩ B = ∅ ∧ C ∪ B = A ∪ B