Theorem difundir 4280

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 4275	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶)))
2		invdif 4268	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶)
3		invdif 4268	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶)
4		invdif 4268	. . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶)
5	3, 4	uneq12i 4161	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))
6	1, 2, 5	3eqtr3i 2768	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))

Syntax hints:   = wceq 1541  Vcvv 3474   ∖ cdif 3945   ∪ cun 3946   ∩ cin 3947

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955

This theorem is referenced by:  dfsymdif3  4296  difun2  4480  diftpsn3  4805  strleun  17092  setsfun0  17107  mreexmrid  17589  mreexexlem2d  17591  mvdco  19315  dprd2da  19914  dmdprdsplit2lem  19917  ablfac1eulem  19944  lbsextlem4  20780  opsrtoslem2  21623  nulmbl2  25060  uniioombllem3  25109  sltlpss  27409  slelss  27410  ex-dif  29714  indifundif  31800  imadifxp  31870  fzodif1  32042  cycpmrn  32343  ballotlemfp1  33559  ballotlemgun  33592  onint1  35420  lindsadd  36567  lindsenlbs  36569  poimirlem2  36576  poimirlem6  36580  poimirlem7  36581  poimirlem8  36582  poimirlem22  36596  dvmptfprodlem  44739  fourierdlem102  45003  fourierdlem114  45015  caragenuncllem  45307  carageniuncllem1  45316