Theorem difundir 4222

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 4217	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶)))
2		invdif 4210	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶)
3		invdif 4210	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶)
4		invdif 4210	. . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶)
5	3, 4	uneq12i 4099	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))
6	1, 2, 5	3eqtr3i 2772	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))

Syntax hints:   = wceq 1548  Vcvv 3433   ∖ cdif 3882   ∪ cun 3883   ∩ cin 3884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892

This theorem is referenced by:  dfsymdif3  4237  difun2  4412  diftpsn3  4738  strleun  17122  setsfun0  17137  mreexmrid  17604  mreexexlem2d  17606  chnccats1  18586  mvdco  19415  dprd2da  20014  dmdprdsplit2lem  20017  ablfac1eulem  20044  lbsextlem4  21158  opsrtoslem2  22036  nulmbl2  25525  uniioombllem3  25574  ltslpss  27922  leslss  27923  ex-dif  30515  indifundif  32616  imadifxp  32694  fzodif1  32888  cycpmrn  33228  ballotlemfp1  34688  ballotlemgun  34721  onint1  36692  lindsadd  37995  lindsenlbs  37997  poimirlem2  38004  poimirlem6  38008  poimirlem7  38009  poimirlem8  38010  poimirlem22  38024  dmxrnuncnvepres  38774  dvmptfprodlem  46401  fourierdlem102  46665  fourierdlem114  46677  caragenuncllem  46969  carageniuncllem1  46978