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