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

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

Proof of Theorem difundir
StepHypRef Expression
1 indir 4274 . 2 ((𝐴𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶)))
2 invdif 4267 . 2 ((𝐴𝐵) ∩ (V ∖ 𝐶)) = ((𝐴𝐵) ∖ 𝐶)
3 invdif 4267 . . 3 (𝐴 ∩ (V ∖ 𝐶)) = (𝐴𝐶)
4 invdif 4267 . . 3 (𝐵 ∩ (V ∖ 𝐶)) = (𝐵𝐶)
53, 4uneq12i 4158 . 2 ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴𝐶) ∪ (𝐵𝐶))
61, 2, 53eqtr3i 2762 1 ((𝐴𝐵) ∖ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1534  Vcvv 3462  cdif 3943  cun 3944  cin 3945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-v 3464  df-dif 3949  df-un 3951  df-in 3953
This theorem is referenced by:  dfsymdif3  4295  difun2  4475  diftpsn3  4801  strleun  17154  setsfun0  17169  mreexmrid  17651  mreexexlem2d  17653  mvdco  19439  dprd2da  20038  dmdprdsplit2lem  20041  ablfac1eulem  20068  lbsextlem4  21138  opsrtoslem2  22065  nulmbl2  25553  uniioombllem3  25602  sltlpss  27927  slelss  27928  ex-dif  30353  indifundif  32452  imadifxp  32521  fzodif1  32698  cycpmrn  33025  ballotlemfp1  34338  ballotlemgun  34371  onint1  36174  lindsadd  37327  lindsenlbs  37329  poimirlem2  37336  poimirlem6  37340  poimirlem7  37341  poimirlem8  37342  poimirlem22  37356  dvmptfprodlem  45601  fourierdlem102  45865  fourierdlem114  45877  caragenuncllem  46169  carageniuncllem1  46178
  Copyright terms: Public domain W3C validator