Theorem difundir 4242

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 4237	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶)))
2		invdif 4230	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶)
3		invdif 4230	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶)
4		invdif 4230	. . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶)
5	3, 4	uneq12i 4117	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))
6	1, 2, 5	3eqtr3i 2760	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))

Syntax hints:   = wceq 1540  Vcvv 3436   ∖ cdif 3900   ∪ cun 3901   ∩ cin 3902

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910

This theorem is referenced by:  dfsymdif3  4257  difun2  4432  diftpsn3  4753  strleun  17068  setsfun0  17083  mreexmrid  17549  mreexexlem2d  17551  mvdco  19324  dprd2da  19923  dmdprdsplit2lem  19926  ablfac1eulem  19953  lbsextlem4  21068  opsrtoslem2  21961  nulmbl2  25435  uniioombllem3  25484  sltlpss  27822  slelss  27823  ex-dif  30367  indifundif  32468  imadifxp  32545  fzodif1  32736  chnccats1  32958  cycpmrn  33086  ballotlemfp1  34466  ballotlemgun  34499  onint1  36433  lindsadd  37603  lindsenlbs  37605  poimirlem2  37612  poimirlem6  37616  poimirlem7  37617  poimirlem8  37618  poimirlem22  37632  dvmptfprodlem  45935  fourierdlem102  46199  fourierdlem114  46211  caragenuncllem  46503  carageniuncllem1  46512