Theorem difundir 4245

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

Syntax hints:   = wceq 1542  Vcvv 3442   ∖ cdif 3900   ∪ cun 3901   ∩ cin 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910

This theorem is referenced by:  dfsymdif3  4260  difun2  4435  diftpsn3  4760  strleun  17098  setsfun0  17113  mreexmrid  17580  mreexexlem2d  17582  chnccats1  18562  mvdco  19391  dprd2da  19990  dmdprdsplit2lem  19993  ablfac1eulem  20020  lbsextlem4  21133  opsrtoslem2  22028  nulmbl2  25510  uniioombllem3  25559  ltslpss  27921  leslss  27922  ex-dif  30516  indifundif  32617  imadifxp  32694  fzodif1  32889  cycpmrn  33243  ballotlemfp1  34676  ballotlemgun  34709  onint1  36671  lindsadd  37893  lindsenlbs  37895  poimirlem2  37902  poimirlem6  37906  poimirlem7  37907  poimirlem8  37908  poimirlem22  37922  dmxrnuncnvepres  38672  dvmptfprodlem  46331  fourierdlem102  46595  fourierdlem114  46607  caragenuncllem  46899  carageniuncllem1  46908