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

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

Proof of Theorem difundir
StepHypRef Expression
1 indir 4285 . 2 ((𝐴𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶)))
2 invdif 4278 . 2 ((𝐴𝐵) ∩ (V ∖ 𝐶)) = ((𝐴𝐵) ∖ 𝐶)
3 invdif 4278 . . 3 (𝐴 ∩ (V ∖ 𝐶)) = (𝐴𝐶)
4 invdif 4278 . . 3 (𝐵 ∩ (V ∖ 𝐶)) = (𝐵𝐶)
53, 4uneq12i 4165 . 2 ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴𝐶) ∪ (𝐵𝐶))
61, 2, 53eqtr3i 2772 1 ((𝐴𝐵) ∖ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1539  Vcvv 3479  cdif 3947  cun 3948  cin 3949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-in 3957
This theorem is referenced by:  dfsymdif3  4305  difun2  4480  diftpsn3  4801  strleun  17195  setsfun0  17210  mreexmrid  17687  mreexexlem2d  17689  mvdco  19464  dprd2da  20063  dmdprdsplit2lem  20066  ablfac1eulem  20093  lbsextlem4  21164  opsrtoslem2  22081  nulmbl2  25572  uniioombllem3  25621  sltlpss  27946  slelss  27947  ex-dif  30443  indifundif  32544  imadifxp  32615  fzodif1  32795  chnccats1  33006  cycpmrn  33164  ballotlemfp1  34495  ballotlemgun  34528  onint1  36451  lindsadd  37621  lindsenlbs  37623  poimirlem2  37630  poimirlem6  37634  poimirlem7  37635  poimirlem8  37636  poimirlem22  37650  dvmptfprodlem  45964  fourierdlem102  46228  fourierdlem114  46240  caragenuncllem  46532  carageniuncllem1  46541
  Copyright terms: Public domain W3C validator