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 ( ( 𝐴 ∖ 𝐵 ) = 𝐶 ↔ ( ( 𝐶 ∩ 𝐵 ) = ∅ ∧ ( 𝐶 ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 ) ) )

Proof

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