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

Metamath Proof Explorer

Theorem difindi

Description: Distributive law for class difference. Theorem 40 of Suppes p. 29. (Contributed by NM, 17-Aug-2004)

Ref Expression
Assertion difindi ⊢ A ∖ B ∩ C = A ∖ B ∪ A ∖ C

Proof

Step Hyp Ref Expression
1 dfin3 ⊢ B ∩ C = V ∖ V ∖ B ∪ V ∖ C
2 1 difeq2i ⊢ A ∖ B ∩ C = A ∖ V ∖ V ∖ B ∪ V ∖ C
3 indi ⊢ A ∩ V ∖ B ∪ V ∖ C = A ∩ V ∖ B ∪ A ∩ V ∖ C
4 dfin2 ⊢ A ∩ V ∖ B ∪ V ∖ C = A ∖ V ∖ V ∖ B ∪ V ∖ C
5 invdif ⊢ A ∩ V ∖ B = A ∖ B
6 invdif ⊢ A ∩ V ∖ C = A ∖ C
7 5 6 uneq12i ⊢ A ∩ V ∖ B ∪ A ∩ V ∖ C = A ∖ B ∪ A ∖ C
8 3 4 7 3eqtr3i ⊢ A ∖ V ∖ V ∖ B ∪ V ∖ C = A ∖ B ∪ A ∖ C
9 2 8 eqtri ⊢ A ∖ B ∩ C = A ∖ B ∪ A ∖ C