Theorem difundir 4232

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 4227	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶)))
2		invdif 4220	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶)
3		invdif 4220	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶)
4		invdif 4220	. . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶)
5	3, 4	uneq12i 4107	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))
6	1, 2, 5	3eqtr3i 2768	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))

Syntax hints:   = wceq 1542  Vcvv 3430   ∖ cdif 3887   ∪ cun 3888   ∩ cin 3889

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897

This theorem is referenced by:  dfsymdif3  4247  difun2  4422  diftpsn3  4746  strleun  17122  setsfun0  17137  mreexmrid  17604  mreexexlem2d  17606  chnccats1  18586  mvdco  19415  dprd2da  20014  dmdprdsplit2lem  20017  ablfac1eulem  20044  lbsextlem4  21155  opsrtoslem2  22048  nulmbl2  25517  uniioombllem3  25566  ltslpss  27918  leslss  27919  ex-dif  30512  indifundif  32613  imadifxp  32690  fzodif1  32884  cycpmrn  33223  ballotlemfp1  34656  ballotlemgun  34689  onint1  36651  lindsadd  37952  lindsenlbs  37954  poimirlem2  37961  poimirlem6  37965  poimirlem7  37966  poimirlem8  37967  poimirlem22  37981  dmxrnuncnvepres  38731  dvmptfprodlem  46394  fourierdlem102  46658  fourierdlem114  46670  caragenuncllem  46962  carageniuncllem1  46971