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

Proof

Step Hyp Ref Expression
1 dfin3 ⊢ ( 𝐵 ∩ 𝐶 ) = ( V ∖ ( ( V ∖ 𝐵 ) ∪ ( V ∖ 𝐶 ) ) )
2 1 difeq2i ⊢ ( 𝐴 ∖ ( 𝐵 ∩ 𝐶 ) ) = ( 𝐴 ∖ ( V ∖ ( ( V ∖ 𝐵 ) ∪ ( V ∖ 𝐶 ) ) ) )
3 indi ⊢ ( 𝐴 ∩ ( ( V ∖ 𝐵 ) ∪ ( V ∖ 𝐶 ) ) ) = ( ( 𝐴 ∩ ( V ∖ 𝐵 ) ) ∪ ( 𝐴 ∩ ( V ∖ 𝐶 ) ) )
4 dfin2 ⊢ ( 𝐴 ∩ ( ( V ∖ 𝐵 ) ∪ ( V ∖ 𝐶 ) ) ) = ( 𝐴 ∖ ( V ∖ ( ( V ∖ 𝐵 ) ∪ ( V ∖ 𝐶 ) ) ) )
5 invdif ⊢ ( 𝐴 ∩ ( V ∖ 𝐵 ) ) = ( 𝐴 ∖ 𝐵 )
6 invdif ⊢ ( 𝐴 ∩ ( V ∖ 𝐶 ) ) = ( 𝐴 ∖ 𝐶 )
7 5 6 uneq12i ⊢ ( ( 𝐴 ∩ ( V ∖ 𝐵 ) ) ∪ ( 𝐴 ∩ ( V ∖ 𝐶 ) ) ) = ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐴 ∖ 𝐶 ) )
8 3 4 7 3eqtr3i ⊢ ( 𝐴 ∖ ( V ∖ ( ( V ∖ 𝐵 ) ∪ ( V ∖ 𝐶 ) ) ) ) = ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐴 ∖ 𝐶 ) )
9 2 8 eqtri ⊢ ( 𝐴 ∖ ( 𝐵 ∩ 𝐶 ) ) = ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐴 ∖ 𝐶 ) )