Theorem difindi 4267

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 4252	. . 3 ⊢ (𝐵 ∩ 𝐶) = (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶)))
2	1	difeq2i 4098	. 2 ⊢ (𝐴 ∖ (𝐵 ∩ 𝐶)) = (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))))
3		indi 4259	. . 3 ⊢ (𝐴 ∩ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))) = ((𝐴 ∩ (V ∖ 𝐵)) ∪ (𝐴 ∩ (V ∖ 𝐶)))
4		dfin2 4246	. . 3 ⊢ (𝐴 ∩ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))) = (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))))
5		invdif 4254	. . . 4 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
6		invdif 4254	. . . 4 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶)
7	5, 6	uneq12i 4141	. . 3 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ (𝐴 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶))
8	3, 4, 7	3eqtr3i 2766	. 2 ⊢ (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶)))) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶))
9	2, 8	eqtri 2758	1 ⊢ (𝐴 ∖ (𝐵 ∩ 𝐶)) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶))

Syntax hints:   = wceq 1540  Vcvv 3459   ∖ cdif 3923   ∪ cun 3924   ∩ cin 3925

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933

This theorem is referenced by:  difdif2  4271  indm  4273  fndifnfp  7168  dprddisj2  20022  fctop  22942  cctop  22944  mretopd  23030  restcld  23110  cfinfil  23831  csdfil  23832  indifundif  32505  difres  32581  unelcarsg  34344  clsk3nimkb  44064  ntrclskb  44093  ntrclsk3  44094  ntrclsk13  44095  salincl  46353  iscnrm3rlem1  48914