Theorem difundir 4250

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

Syntax hints:   = wceq 1540  Vcvv 3444   ∖ cdif 3908   ∪ cun 3909   ∩ cin 3910

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918

This theorem is referenced by:  dfsymdif3  4265  difun2  4440  diftpsn3  4762  strleun  17103  setsfun0  17118  mreexmrid  17584  mreexexlem2d  17586  mvdco  19359  dprd2da  19958  dmdprdsplit2lem  19961  ablfac1eulem  19988  lbsextlem4  21103  opsrtoslem2  21996  nulmbl2  25470  uniioombllem3  25519  sltlpss  27857  slelss  27858  ex-dif  30402  indifundif  32503  imadifxp  32580  fzodif1  32765  chnccats1  32987  cycpmrn  33115  ballotlemfp1  34476  ballotlemgun  34509  onint1  36430  lindsadd  37600  lindsenlbs  37602  poimirlem2  37609  poimirlem6  37613  poimirlem7  37614  poimirlem8  37615  poimirlem22  37629  dvmptfprodlem  45935  fourierdlem102  46199  fourierdlem114  46211  caragenuncllem  46503  carageniuncllem1  46512