Theorem difundir 4245

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 4240	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶)))
2		invdif 4233	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶)
3		invdif 4233	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶)
4		invdif 4233	. . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶)
5	3, 4	uneq12i 4121	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))
6	1, 2, 5	3eqtr3i 2795	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))

Syntax hints:   = wceq 1562  Vcvv 3456   ∖ cdif 3903   ∪ cun 3904   ∩ cin 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-in 3913

This theorem is referenced by:  dfsymdif3  4260  difun2  4437  diftpsn3  4764  strleun  17195  setsfun0  17210  mreexmrid  17677  mreexexlem2d  17679  chnccats1  18659  mvdco  19487  dprd2da  20086  dmdprdsplit2lem  20089  ablfac1eulem  20116  lbsextlem4  21233  opsrtoslem2  22111  nulmbl2  25600  uniioombllem3  25649  ltslpss  28003  leslss  28004  ex-dif  30627  indifundif  32725  imadifxp  32803  fzodif1  32996  cycpmrn  33325  ballotlemfp1  34791  ballotlemgun  34824  onint1  36814  lindsadd  38117  lindsenlbs  38119  poimirlem2  38126  poimirlem6  38130  poimirlem7  38131  poimirlem8  38132  poimirlem22  38146  dmxrnuncnvepres  38896  dvmptfprodlem  46523  fourierdlem102  46787  fourierdlem114  46799  caragenuncllem  47091  carageniuncllem1  47100