Theorem difindi 4251

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 4236	. . 3 ⊢ (𝐵 ∩ 𝐶) = (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶)))
2	1	difeq2i 4082	. 2 ⊢ (𝐴 ∖ (𝐵 ∩ 𝐶)) = (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))))
3		indi 4243	. . 3 ⊢ (𝐴 ∩ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))) = ((𝐴 ∩ (V ∖ 𝐵)) ∪ (𝐴 ∩ (V ∖ 𝐶)))
4		dfin2 4230	. . 3 ⊢ (𝐴 ∩ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))) = (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))))
5		invdif 4238	. . . 4 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
6		invdif 4238	. . . 4 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶)
7	5, 6	uneq12i 4125	. . 3 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ (𝐴 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶))
8	3, 4, 7	3eqtr3i 2760	. 2 ⊢ (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶)))) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶))
9	2, 8	eqtri 2752	1 ⊢ (𝐴 ∖ (𝐵 ∩ 𝐶)) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶))

Syntax hints:   = wceq 1540  Vcvv 3444   ∖ cdif 3908   ∪ cun 3909   ∩ cin 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918

This theorem is referenced by:  difdif2  4255  indm  4257  fndifnfp  7132  dprddisj2  19955  fctop  22924  cctop  22926  mretopd  23012  restcld  23092  cfinfil  23813  csdfil  23814  indifundif  32503  difres  32579  unelcarsg  34296  clsk3nimkb  44022  ntrclskb  44051  ntrclsk3  44052  ntrclsk13  44053  salincl  46315  iscnrm3rlem1  48921