MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  difundir Structured version   Visualization version   GIF version

Theorem difundir 4245
Description: Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
Assertion
Ref Expression
difundir ((𝐴𝐵) ∖ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))

Proof of Theorem difundir
StepHypRef Expression
1 indir 4240 . 2 ((𝐴𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶)))
2 invdif 4233 . 2 ((𝐴𝐵) ∩ (V ∖ 𝐶)) = ((𝐴𝐵) ∖ 𝐶)
3 invdif 4233 . . 3 (𝐴 ∩ (V ∖ 𝐶)) = (𝐴𝐶)
4 invdif 4233 . . 3 (𝐵 ∩ (V ∖ 𝐶)) = (𝐵𝐶)
53, 4uneq12i 4126 . 2 ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴𝐶) ∪ (𝐵𝐶))
61, 2, 53eqtr3i 2767 1 ((𝐴𝐵) ∖ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  Vcvv 3446  cdif 3910  cun 3911  cin 3912
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920
This theorem is referenced by:  dfsymdif3  4261  difun2  4445  diftpsn3  4767  strleun  17040  setsfun0  17055  mreexmrid  17537  mreexexlem2d  17539  mvdco  19241  dprd2da  19835  dmdprdsplit2lem  19838  ablfac1eulem  19865  lbsextlem4  20681  opsrtoslem2  21500  nulmbl2  24937  uniioombllem3  24986  sltlpss  27279  ex-dif  29430  indifundif  31516  imadifxp  31586  fzodif1  31764  cycpmrn  32062  ballotlemfp1  33180  ballotlemgun  33213  onint1  34997  lindsadd  36144  lindsenlbs  36146  poimirlem2  36153  poimirlem6  36157  poimirlem7  36158  poimirlem8  36159  poimirlem22  36173  dvmptfprodlem  44305  fourierdlem102  44569  fourierdlem114  44581  caragenuncllem  44873  carageniuncllem1  44882
  Copyright terms: Public domain W3C validator