This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 disj3 ⊢ C ∩ B = ∅ ↔ C = C ∖ B
9 eqcom ⊢ C = C ∖ B ↔ C ∖ B = C
10 8 9 bitri ⊢ C ∩ B = ∅ ↔ C ∖ B = C
11 10 birani ⊢ C ∩ B = ∅ ∧ C ∪ B = A ∪ B → C ∖ B = C
12 difeq1 ⊢ C ∪ B = A ∪ B → C ∪ B ∖ B = A ∪ B ∖ B
13 difun2 ⊢ C ∪ B ∖ B = C ∖ B
14 difun2 ⊢ A ∪ B ∖ B = A ∖ B
15 12 13 14 3eqtr3g ⊢ C ∪ B = A ∪ B → C ∖ B = A ∖ B
16 15 eqeq1d ⊢ C ∪ B = A ∪ B → C ∖ B = C ↔ A ∖ B = C
17 16 adantl ⊢ C ∩ B = ∅ ∧ C ∪ B = A ∪ B → C ∖ B = C ↔ A ∖ B = C
18 11 17 mpbid ⊢ C ∩ B = ∅ ∧ C ∪ B = A ∪ B → A ∖ B = C
19 7 18 impbii ⊢ A ∖ B = C ↔ C ∩ B = ∅ ∧ C ∪ B = A ∪ B