Theorem difundir 4243

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 4238	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶)))
2		invdif 4231	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶)
3		invdif 4231	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶)
4		invdif 4231	. . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶)
5	3, 4	uneq12i 4119	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))
6	1, 2, 5	3eqtr3i 2793	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))

This proof depends on syntax axioms:   = wceq 1569  Vcvv 3454   ∖ cdif 3901   ∪ cun 3902   ∩ cin 3903

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911

This theorem is used by:  dfsymdif3  4258  difun2  4441  diftpsn3  4769  strleun  17223  setsfun0  17238  mreexmrid  17705  mreexexlem2d  17707  chnccats1  18687  mvdco  19521  dprd2da  20120  dmdprdsplit2lem  20123  ablfac1eulem  20150  lbsextlem4  21296  opsrtoslem2  22218  nulmbl2  25706  uniioombllem3  25755  ltslpss  28112  leslss  28113  ex-dif  30785  indifundif  32881  imadifxp  32957  fzodif1  33148  cycpmrn  33472  ballotlemfp1  34891  ballotlemgun  34924  onint1  36988  lindsadd  38292  lindsenlbs  38294  poimirlem2  38301  poimirlem6  38305  poimirlem7  38306  poimirlem8  38307  poimirlem22  38321  dmxrnuncnvepres  39069  dvmptfprodlem  46686  fourierdlem102  46950  fourierdlem114  46962  caragenuncllem  47254  carageniuncllem1  47263