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

Metamath Proof Explorer

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