Theorem difundir 4238

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 4233	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶)))
2		invdif 4226	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶)
3		invdif 4226	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶)
4		invdif 4226	. . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶)
5	3, 4	uneq12i 4113	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))
6	1, 2, 5	3eqtr3i 2760	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))

Syntax hints:   = wceq 1540  Vcvv 3433   ∖ cdif 3896   ∪ cun 3897   ∩ cin 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3393  df-v 3435  df-dif 3902  df-un 3904  df-in 3906

This theorem is referenced by:  dfsymdif3  4253  difun2  4428  diftpsn3  4751  strleun  17055  setsfun0  17070  mreexmrid  17536  mreexexlem2d  17538  mvdco  19311  dprd2da  19910  dmdprdsplit2lem  19913  ablfac1eulem  19940  lbsextlem4  21052  opsrtoslem2  21945  nulmbl2  25418  uniioombllem3  25467  sltlpss  27807  slelss  27808  ex-dif  30354  indifundif  32456  imadifxp  32533  fzodif1  32727  chnccats1  32952  cycpmrn  33080  ballotlemfp1  34473  ballotlemgun  34506  onint1  36440  lindsadd  37610  lindsenlbs  37612  poimirlem2  37619  poimirlem6  37623  poimirlem7  37624  poimirlem8  37625  poimirlem22  37639  dvmptfprodlem  45939  fourierdlem102  46203  fourierdlem114  46215  caragenuncllem  46507  carageniuncllem1  46516