Theorem difundir 4219

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 4214	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶)))
2		invdif 4207	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶)
3		invdif 4207	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶)
4		invdif 4207	. . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶)
5	3, 4	uneq12i 4099	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))
6	1, 2, 5	3eqtr3i 2775	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))

Syntax hints:   = wceq 1541  Vcvv 3430   ∖ cdif 3888   ∪ cun 3889   ∩ cin 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898

This theorem is referenced by:  dfsymdif3  4235  difun2  4419  diftpsn3  4740  strleun  16839  setsfun0  16854  mreexmrid  17333  mreexexlem2d  17335  mvdco  19034  dprd2da  19626  dmdprdsplit2lem  19629  ablfac1eulem  19656  lbsextlem4  20404  opsrtoslem2  21244  nulmbl2  24681  uniioombllem3  24730  ex-dif  28766  indifundif  30852  imadifxp  30919  fzodif1  31093  cycpmrn  31389  ballotlemfp1  32437  ballotlemgun  32470  sltlpss  34066  onint1  34617  lindsadd  35749  lindsenlbs  35751  poimirlem2  35758  poimirlem6  35762  poimirlem7  35763  poimirlem8  35764  poimirlem22  35778  dvmptfprodlem  43439  fourierdlem102  43703  fourierdlem114  43715  caragenuncllem  44004  carageniuncllem1  44013