Theorem difundir 4310

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 4305	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶)))
2		invdif 4298	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶)
3		invdif 4298	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶)
4		invdif 4298	. . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶)
5	3, 4	uneq12i 4189	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))
6	1, 2, 5	3eqtr3i 2776	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))

Syntax hints:   = wceq 1537  Vcvv 3488   ∖ cdif 3973   ∪ cun 3974   ∩ cin 3975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983

This theorem is referenced by:  dfsymdif3  4325  difun2  4504  diftpsn3  4827  strleun  17204  setsfun0  17219  mreexmrid  17701  mreexexlem2d  17703  mvdco  19487  dprd2da  20086  dmdprdsplit2lem  20089  ablfac1eulem  20116  lbsextlem4  21186  opsrtoslem2  22103  nulmbl2  25590  uniioombllem3  25639  sltlpss  27963  slelss  27964  ex-dif  30455  indifundif  32554  imadifxp  32623  fzodif1  32798  cycpmrn  33136  ballotlemfp1  34456  ballotlemgun  34489  onint1  36415  lindsadd  37573  lindsenlbs  37575  poimirlem2  37582  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem22  37602  dvmptfprodlem  45865  fourierdlem102  46129  fourierdlem114  46141  caragenuncllem  46433  carageniuncllem1  46442