Theorem difundir 4244

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 4239	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶)))
2		invdif 4232	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶)
3		invdif 4232	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶)
4		invdif 4232	. . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶)
5	3, 4	uneq12i 4120	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))
6	1, 2, 5	3eqtr3i 2794	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))

This proof depends on syntax axioms:   = wceq 1570  Vcvv 3455   ∖ cdif 3902   ∪ cun 3903   ∩ cin 3904

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912

This theorem is used by:  dfsymdif3  4259  difun2  4442  diftpsn3  4770  strleun  17221  setsfun0  17236  mreexmrid  17703  mreexexlem2d  17705  chnccats1  18685  mvdco  19519  dprd2da  20118  dmdprdsplit2lem  20121  ablfac1eulem  20148  lbsextlem4  21294  opsrtoslem2  22216  nulmbl2  25704  uniioombllem3  25753  ltslpss  28110  leslss  28111  ex-dif  30783  indifundif  32879  imadifxp  32955  fzodif1  33146  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