Theorem indifundif

Description: A remarkable equation with sets. (Contributed by Thierry Arnoux, 18-May-2020)

	Ref	Expression
Assertion	indifundif	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 ) ∪ ( 𝐴 ∖ 𝐵 ) ) = ( 𝐴 ∖ ( 𝐵 ∩ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		difindi	⊢ ( 𝐴 ∖ ( 𝐵 ∩ 𝐶 ) ) = ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐴 ∖ 𝐶 ) )
2		difundir	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ∖ 𝐶 ) = ( ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 ) ∪ ( ( 𝐴 ∖ 𝐵 ) ∖ 𝐶 ) )
3		inundif	⊢ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴
4	3	difeq1i	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ∖ 𝐶 ) = ( 𝐴 ∖ 𝐶 )
5		uncom	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 ) ∪ ( ( 𝐴 ∖ 𝐵 ) ∖ 𝐶 ) ) = ( ( ( 𝐴 ∖ 𝐵 ) ∖ 𝐶 ) ∪ ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 ) )
6	2 4 5	3eqtr3i	⊢ ( 𝐴 ∖ 𝐶 ) = ( ( ( 𝐴 ∖ 𝐵 ) ∖ 𝐶 ) ∪ ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 ) )
7	6	uneq2i	⊢ ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐴 ∖ 𝐶 ) ) = ( ( 𝐴 ∖ 𝐵 ) ∪ ( ( ( 𝐴 ∖ 𝐵 ) ∖ 𝐶 ) ∪ ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 ) ) )
8		unass	⊢ ( ( ( 𝐴 ∖ 𝐵 ) ∪ ( ( 𝐴 ∖ 𝐵 ) ∖ 𝐶 ) ) ∪ ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 ) ) = ( ( 𝐴 ∖ 𝐵 ) ∪ ( ( ( 𝐴 ∖ 𝐵 ) ∖ 𝐶 ) ∪ ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 ) ) )
9		undifabs	⊢ ( ( 𝐴 ∖ 𝐵 ) ∪ ( ( 𝐴 ∖ 𝐵 ) ∖ 𝐶 ) ) = ( 𝐴 ∖ 𝐵 )
10	9	uneq1i	⊢ ( ( ( 𝐴 ∖ 𝐵 ) ∪ ( ( 𝐴 ∖ 𝐵 ) ∖ 𝐶 ) ) ∪ ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 ) ) = ( ( 𝐴 ∖ 𝐵 ) ∪ ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 ) )
11	7 8 10	3eqtr2i	⊢ ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐴 ∖ 𝐶 ) ) = ( ( 𝐴 ∖ 𝐵 ) ∪ ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 ) )
12		uncom	⊢ ( ( 𝐴 ∖ 𝐵 ) ∪ ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 ) ) = ( ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 ) ∪ ( 𝐴 ∖ 𝐵 ) )
13	1 11 12	3eqtrri	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 ) ∪ ( 𝐴 ∖ 𝐵 ) ) = ( 𝐴 ∖ ( 𝐵 ∩ 𝐶 ) )