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

Proof

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