Theorem difundir 4241

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 4236	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶)))
2		invdif 4229	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶)
3		invdif 4229	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶)
4		invdif 4229	. . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶)
5	3, 4	uneq12i 4116	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))
6	1, 2, 5	3eqtr3i 2765	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))

Syntax hints:   = wceq 1541  Vcvv 3438   ∖ cdif 3896   ∪ cun 3897   ∩ cin 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906

This theorem is referenced by:  dfsymdif3  4256  difun2  4431  diftpsn3  4756  strleun  17082  setsfun0  17097  mreexmrid  17564  mreexexlem2d  17566  chnccats1  18546  mvdco  19372  dprd2da  19971  dmdprdsplit2lem  19974  ablfac1eulem  20001  lbsextlem4  21114  opsrtoslem2  22009  nulmbl2  25491  uniioombllem3  25540  sltlpss  27880  slelss  27881  ex-dif  30447  indifundif  32548  imadifxp  32625  fzodif1  32821  cycpmrn  33174  ballotlemfp1  34598  ballotlemgun  34631  onint1  36592  lindsadd  37753  lindsenlbs  37755  poimirlem2  37762  poimirlem6  37766  poimirlem7  37767  poimirlem8  37768  poimirlem22  37782  dmxrnuncnvepres  38516  dvmptfprodlem  46130  fourierdlem102  46394  fourierdlem114  46406  caragenuncllem  46698  carageniuncllem1  46707