Theorem difundir 4236

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

This proof depends on syntax axioms:   = wceq 1569  Vcvv 3450   ∖ cdif 4045   ∩ cin 4089   ∪ cun 4149

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 4047  df-in 4091  df-un 4151

This theorem is used by:  dfsymdif3  4251  difun2  4436  diftpsn3  4764  strleun  17335  setsfun0  17350  mreexmrid  17817  mreexexlem2d  17819  chnccats1  18799  mvdco  19659  dprd2da  20258  dmdprdsplit2lem  20261  ablfac1eulem  20288  lbsextlem4  21439  lindsenlbs  22157  opsrtoslem2  22365  nulmbl2  25857  uniioombllem3  25906  ltslpss  28294  leslss  28295  ex-dif  31024  indifundif  33120  imadifxp  33195  fzodif1  33384  cycpmrn  33704  ballotlemfp1  35124  ballotlemgun  35157  onint1  37237  lindsadd  38537  poimirlem2  38541  poimirlem6  38545  poimirlem7  38546  poimirlem8  38547  poimirlem22  38561  dmxrnuncnvepres  39325  dvmptfprodlem  46954  fourierdlem102  47218  fourierdlem114  47230  caragenuncllem  47522  carageniuncllem1  47531