Theorem difundir 4207

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 4202	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶)))
2		invdif 4195	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶)
3		invdif 4195	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶)
4		invdif 4195	. . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶)
5	3, 4	uneq12i 4088	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))
6	1, 2, 5	3eqtr3i 2829	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))

Syntax hints:   = wceq 1538  Vcvv 3441   ∖ cdif 3878   ∪ cun 3879   ∩ cin 3880

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888

This theorem is referenced by:  dfsymdif3  4221  difun2  4387  diftpsn3  4695  setsfun0  16511  strleun  16583  mreexmrid  16906  mreexexlem2d  16908  mvdco  18565  dprd2da  19157  dmdprdsplit2lem  19160  ablfac1eulem  19187  lbsextlem4  19926  opsrtoslem2  20724  nulmbl2  24140  uniioombllem3  24189  ex-dif  28208  indifundif  30297  imadifxp  30364  fzodif1  30542  cycpmrn  30835  ballotlemfp1  31859  ballotlemgun  31892  onint1  33910  lindsadd  35050  lindsenlbs  35052  poimirlem2  35059  poimirlem6  35063  poimirlem7  35064  poimirlem8  35065  poimirlem22  35079  dvmptfprodlem  42586  fourierdlem102  42850  fourierdlem114  42862  caragenuncllem  43151  carageniuncllem1  43160