Theorem difundir 4271

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 4266	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶)))
2		invdif 4259	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶)
3		invdif 4259	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶)
4		invdif 4259	. . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶)
5	3, 4	uneq12i 4146	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))
6	1, 2, 5	3eqtr3i 2767	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))

Syntax hints:   = wceq 1540  Vcvv 3464   ∖ cdif 3928   ∪ cun 3929   ∩ cin 3930

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938

This theorem is referenced by:  dfsymdif3  4286  difun2  4461  diftpsn3  4783  strleun  17181  setsfun0  17196  mreexmrid  17660  mreexexlem2d  17662  mvdco  19431  dprd2da  20030  dmdprdsplit2lem  20033  ablfac1eulem  20060  lbsextlem4  21127  opsrtoslem2  22019  nulmbl2  25494  uniioombllem3  25543  sltlpss  27876  slelss  27877  ex-dif  30409  indifundif  32510  imadifxp  32587  fzodif1  32774  chnccats1  33000  cycpmrn  33159  ballotlemfp1  34529  ballotlemgun  34562  onint1  36472  lindsadd  37642  lindsenlbs  37644  poimirlem2  37651  poimirlem6  37655  poimirlem7  37656  poimirlem8  37657  poimirlem22  37671  dvmptfprodlem  45940  fourierdlem102  46204  fourierdlem114  46216  caragenuncllem  46508  carageniuncllem1  46517