Metamath Proof Explorer

Theorem difdifdir

Description: Distributive law for class difference. Exercise 4.8 of Stoll p. 16. (Contributed by NM, 18-Aug-2004)

Ref Expression
Assertion difdifdir ( ( 𝐴 ∖ 𝐵 ) ∖ 𝐶 ) = ( ( 𝐴 ∖ 𝐶 ) ∖ ( 𝐵 ∖ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 dif32 ⊢ ( ( 𝐴 ∖ 𝐵 ) ∖ 𝐶 ) = ( ( 𝐴 ∖ 𝐶 ) ∖ 𝐵 )
2 invdif ⊢ ( ( 𝐴 ∖ 𝐶 ) ∩ ( V ∖ 𝐵 ) ) = ( ( 𝐴 ∖ 𝐶 ) ∖ 𝐵 )
3 1 2 eqtr4i ⊢ ( ( 𝐴 ∖ 𝐵 ) ∖ 𝐶 ) = ( ( 𝐴 ∖ 𝐶 ) ∩ ( V ∖ 𝐵 ) )
4 un0 ⊢ ( ( ( 𝐴 ∖ 𝐶 ) ∩ ( V ∖ 𝐵 ) ) ∪ ∅ ) = ( ( 𝐴 ∖ 𝐶 ) ∩ ( V ∖ 𝐵 ) )
5 3 4 eqtr4i ⊢ ( ( 𝐴 ∖ 𝐵 ) ∖ 𝐶 ) = ( ( ( 𝐴 ∖ 𝐶 ) ∩ ( V ∖ 𝐵 ) ) ∪ ∅ )
6 indi ⊢ ( ( 𝐴 ∖ 𝐶 ) ∩ ( ( V ∖ 𝐵 ) ∪ 𝐶 ) ) = ( ( ( 𝐴 ∖ 𝐶 ) ∩ ( V ∖ 𝐵 ) ) ∪ ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐶 ) )
7 disjdif ⊢ ( 𝐶 ∩ ( 𝐴 ∖ 𝐶 ) ) = ∅
8 incom ⊢ ( 𝐶 ∩ ( 𝐴 ∖ 𝐶 ) ) = ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐶 )
9 7 8 eqtr3i ⊢ ∅ = ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐶 )
10 9 uneq2i ⊢ ( ( ( 𝐴 ∖ 𝐶 ) ∩ ( V ∖ 𝐵 ) ) ∪ ∅ ) = ( ( ( 𝐴 ∖ 𝐶 ) ∩ ( V ∖ 𝐵 ) ) ∪ ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐶 ) )
11 6 10 eqtr4i ⊢ ( ( 𝐴 ∖ 𝐶 ) ∩ ( ( V ∖ 𝐵 ) ∪ 𝐶 ) ) = ( ( ( 𝐴 ∖ 𝐶 ) ∩ ( V ∖ 𝐵 ) ) ∪ ∅ )
12 5 11 eqtr4i ⊢ ( ( 𝐴 ∖ 𝐵 ) ∖ 𝐶 ) = ( ( 𝐴 ∖ 𝐶 ) ∩ ( ( V ∖ 𝐵 ) ∪ 𝐶 ) )
13 ddif ⊢ ( V ∖ ( V ∖ 𝐶 ) ) = 𝐶
14 13 uneq2i ⊢ ( ( V ∖ 𝐵 ) ∪ ( V ∖ ( V ∖ 𝐶 ) ) ) = ( ( V ∖ 𝐵 ) ∪ 𝐶 )
15 indm ⊢ ( V ∖ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) ) = ( ( V ∖ 𝐵 ) ∪ ( V ∖ ( V ∖ 𝐶 ) ) )
16 invdif ⊢ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) = ( 𝐵 ∖ 𝐶 )
17 16 difeq2i ⊢ ( V ∖ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) ) = ( V ∖ ( 𝐵 ∖ 𝐶 ) )
18 15 17 eqtr3i ⊢ ( ( V ∖ 𝐵 ) ∪ ( V ∖ ( V ∖ 𝐶 ) ) ) = ( V ∖ ( 𝐵 ∖ 𝐶 ) )
19 14 18 eqtr3i ⊢ ( ( V ∖ 𝐵 ) ∪ 𝐶 ) = ( V ∖ ( 𝐵 ∖ 𝐶 ) )
20 19 ineq2i ⊢ ( ( 𝐴 ∖ 𝐶 ) ∩ ( ( V ∖ 𝐵 ) ∪ 𝐶 ) ) = ( ( 𝐴 ∖ 𝐶 ) ∩ ( V ∖ ( 𝐵 ∖ 𝐶 ) ) )
21 invdif ⊢ ( ( 𝐴 ∖ 𝐶 ) ∩ ( V ∖ ( 𝐵 ∖ 𝐶 ) ) ) = ( ( 𝐴 ∖ 𝐶 ) ∖ ( 𝐵 ∖ 𝐶 ) )
22 12 20 21 3eqtri ⊢ ( ( 𝐴 ∖ 𝐵 ) ∖ 𝐶 ) = ( ( 𝐴 ∖ 𝐶 ) ∖ ( 𝐵 ∖ 𝐶 ) )