Theorem difundir 4244

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

Syntax hints:   = wceq 1542  Vcvv 3441   ∖ cdif 3899   ∪ cun 3900   ∩ cin 3901

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 3401  df-v 3443  df-dif 3905  df-un 3907  df-in 3909

This theorem is referenced by:  dfsymdif3  4259  difun2  4434  diftpsn3  4759  strleun  17088  setsfun0  17103  mreexmrid  17570  mreexexlem2d  17572  chnccats1  18552  mvdco  19378  dprd2da  19977  dmdprdsplit2lem  19980  ablfac1eulem  20007  lbsextlem4  21120  opsrtoslem2  22015  nulmbl2  25497  uniioombllem3  25546  ltslpss  27908  leslss  27909  ex-dif  30502  indifundif  32602  imadifxp  32679  fzodif1  32874  cycpmrn  33227  ballotlemfp1  34651  ballotlemgun  34684  onint1  36645  lindsadd  37816  lindsenlbs  37818  poimirlem2  37825  poimirlem6  37829  poimirlem7  37830  poimirlem8  37831  poimirlem22  37845  dmxrnuncnvepres  38595  dvmptfprodlem  46255  fourierdlem102  46519  fourierdlem114  46531  caragenuncllem  46823  carageniuncllem1  46832