Theorem difundir 4231

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

Syntax hints:   = wceq 1542  Vcvv 3429   ∖ cdif 3886   ∪ cun 3887   ∩ cin 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896

This theorem is referenced by:  dfsymdif3  4246  difun2  4421  diftpsn3  4747  strleun  17127  setsfun0  17142  mreexmrid  17609  mreexexlem2d  17611  chnccats1  18591  mvdco  19420  dprd2da  20019  dmdprdsplit2lem  20022  ablfac1eulem  20049  lbsextlem4  21159  opsrtoslem2  22034  nulmbl2  25503  uniioombllem3  25552  ltslpss  27900  leslss  27901  ex-dif  30493  indifundif  32594  imadifxp  32671  fzodif1  32865  cycpmrn  33204  ballotlemfp1  34636  ballotlemgun  34669  onint1  36631  lindsadd  37934  lindsenlbs  37936  poimirlem2  37943  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem22  37963  dmxrnuncnvepres  38713  dvmptfprodlem  46372  fourierdlem102  46636  fourierdlem114  46648  caragenuncllem  46940  carageniuncllem1  46949