Theorem difundir 4290

Description: Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)

Assertion

Ref	Expression
difundir	⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))

Proof of Theorem difundir

Step	Hyp	Ref	Expression
1		indir 4285	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶)))
2		invdif 4278	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶)
3		invdif 4278	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶)
4		invdif 4278	. . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶)
5	3, 4	uneq12i 4165	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))
6	1, 2, 5	3eqtr3i 2772	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))

Syntax hints:   = wceq 1539  Vcvv 3479   ∖ cdif 3947   ∪ cun 3948   ∩ cin 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-in 3957

This theorem is referenced by:  dfsymdif3  4305  difun2  4480  diftpsn3  4801  strleun  17195  setsfun0  17210  mreexmrid  17687  mreexexlem2d  17689  mvdco  19464  dprd2da  20063  dmdprdsplit2lem  20066  ablfac1eulem  20093  lbsextlem4  21164  opsrtoslem2  22081  nulmbl2  25572  uniioombllem3  25621  sltlpss  27946  slelss  27947  ex-dif  30443  indifundif  32544  imadifxp  32615  fzodif1  32795  chnccats1  33006  cycpmrn  33164  ballotlemfp1  34495  ballotlemgun  34528  onint1  36451  lindsadd  37621  lindsenlbs  37623  poimirlem2  37630  poimirlem6  37634  poimirlem7  37635  poimirlem8  37636  poimirlem22  37650  dvmptfprodlem  45964  fourierdlem102  46228  fourierdlem114  46240  caragenuncllem  46532  carageniuncllem1  46541