Theorem difundir 4279

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 4274	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶)))
2		invdif 4267	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶)
3		invdif 4267	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶)
4		invdif 4267	. . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶)
5	3, 4	uneq12i 4158	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))
6	1, 2, 5	3eqtr3i 2762	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))

Syntax hints:   = wceq 1534  Vcvv 3462   ∖ cdif 3943   ∪ cun 3944   ∩ cin 3945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-v 3464  df-dif 3949  df-un 3951  df-in 3953

This theorem is referenced by:  dfsymdif3  4295  difun2  4475  diftpsn3  4801  strleun  17154  setsfun0  17169  mreexmrid  17651  mreexexlem2d  17653  mvdco  19439  dprd2da  20038  dmdprdsplit2lem  20041  ablfac1eulem  20068  lbsextlem4  21138  opsrtoslem2  22065  nulmbl2  25553  uniioombllem3  25602  sltlpss  27927  slelss  27928  ex-dif  30353  indifundif  32452  imadifxp  32521  fzodif1  32698  cycpmrn  33025  ballotlemfp1  34338  ballotlemgun  34371  onint1  36174  lindsadd  37327  lindsenlbs  37329  poimirlem2  37336  poimirlem6  37340  poimirlem7  37341  poimirlem8  37342  poimirlem22  37356  dvmptfprodlem  45601  fourierdlem102  45865  fourierdlem114  45877  caragenuncllem  46169  carageniuncllem1  46178