Theorem difindi 4232

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

Assertion

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

Proof of Theorem difindi

Step	Hyp	Ref	Expression
1		dfin3 4217	. . 3 ⊢ (𝐵 ∩ 𝐶) = (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶)))
2	1	difeq2i 4063	. 2 ⊢ (𝐴 ∖ (𝐵 ∩ 𝐶)) = (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))))
3		indi 4224	. . 3 ⊢ (𝐴 ∩ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))) = ((𝐴 ∩ (V ∖ 𝐵)) ∪ (𝐴 ∩ (V ∖ 𝐶)))
4		dfin2 4211	. . 3 ⊢ (𝐴 ∩ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))) = (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))))
5		invdif 4219	. . . 4 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
6		invdif 4219	. . . 4 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶)
7	5, 6	uneq12i 4106	. . 3 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ (𝐴 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶))
8	3, 4, 7	3eqtr3i 2767	. 2 ⊢ (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶)))) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶))
9	2, 8	eqtri 2759	1 ⊢ (𝐴 ∖ (𝐵 ∩ 𝐶)) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶))

Syntax hints:   = wceq 1542  Vcvv 3429   ∖ cdif 3886   ∪ cun 3887   ∩ cin 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896

This theorem is referenced by:  difdif2  4236  indm  4238  fndifnfp  7131  dprddisj2  20016  fctop  22969  cctop  22971  mretopd  23057  restcld  23137  cfinfil  23858  csdfil  23859  indifundif  32594  difres  32670  unelcarsg  34456  clsk3nimkb  44467  ntrclskb  44496  ntrclsk3  44497  ntrclsk13  44498  salincl  46752  iscnrm3rlem1  49415