Theorem difundir 4257

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 4252	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶)))
2		invdif 4245	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶)
3		invdif 4245	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶)
4		invdif 4245	. . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶)
5	3, 4	uneq12i 4132	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))
6	1, 2, 5	3eqtr3i 2761	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))

Syntax hints:   = wceq 1540  Vcvv 3450   ∖ cdif 3914   ∪ cun 3915   ∩ cin 3916

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924

This theorem is referenced by:  dfsymdif3  4272  difun2  4447  diftpsn3  4769  strleun  17134  setsfun0  17149  mreexmrid  17611  mreexexlem2d  17613  mvdco  19382  dprd2da  19981  dmdprdsplit2lem  19984  ablfac1eulem  20011  lbsextlem4  21078  opsrtoslem2  21970  nulmbl2  25444  uniioombllem3  25493  sltlpss  27826  slelss  27827  ex-dif  30359  indifundif  32460  imadifxp  32537  fzodif1  32722  chnccats1  32948  cycpmrn  33107  ballotlemfp1  34490  ballotlemgun  34523  onint1  36444  lindsadd  37614  lindsenlbs  37616  poimirlem2  37623  poimirlem6  37627  poimirlem7  37628  poimirlem8  37629  poimirlem22  37643  dvmptfprodlem  45949  fourierdlem102  46213  fourierdlem114  46225  caragenuncllem  46517  carageniuncllem1  46526