Theorem difundir 4252

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 4247	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶)))
2		invdif 4240	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶)
3		invdif 4240	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶)
4		invdif 4240	. . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶)
5	3, 4	uneq12i 4128	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))
6	1, 2, 5	3eqtr3i 2800	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))

Syntax hints:   = wceq 1567  Vcvv 3463   ∖ cdif 3910   ∪ cun 3911   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920

This theorem is referenced by:  dfsymdif3  4267  difun2  4447  diftpsn3  4774  strleun  17217  setsfun0  17232  mreexmrid  17699  mreexexlem2d  17701  chnccats1  18681  mvdco  19515  dprd2da  20114  dmdprdsplit2lem  20117  ablfac1eulem  20144  lbsextlem4  21263  opsrtoslem2  22176  nulmbl2  25664  uniioombllem3  25713  ltslpss  28067  leslss  28068  ex-dif  30715  indifundif  32811  imadifxp  32887  fzodif1  33078  cycpmrn  33404  ballotlemfp1  34827  ballotlemgun  34860  onint1  36883  lindsadd  38186  lindsenlbs  38188  poimirlem2  38195  poimirlem6  38199  poimirlem7  38200  poimirlem8  38201  poimirlem22  38215  dmxrnuncnvepres  38965  dvmptfprodlem  46584  fourierdlem102  46848  fourierdlem114  46860  caragenuncllem  47152  carageniuncllem1  47161