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

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

Proof of Theorem difundir
StepHypRef Expression
1 indir 4237 . 2 ((𝐴𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶)))
2 invdif 4230 . 2 ((𝐴𝐵) ∩ (V ∖ 𝐶)) = ((𝐴𝐵) ∖ 𝐶)
3 invdif 4230 . . 3 (𝐴 ∩ (V ∖ 𝐶)) = (𝐴𝐶)
4 invdif 4230 . . 3 (𝐵 ∩ (V ∖ 𝐶)) = (𝐵𝐶)
53, 4uneq12i 4123 . 2 ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴𝐶) ∪ (𝐵𝐶))
61, 2, 53eqtr3i 2855 1 ((𝐴𝐵) ∖ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:   = wceq 1538  Vcvv 3480   ∖ cdif 3916   ∪ cun 3917   ∩ cin 3918 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 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-rab 3142  df-v 3482  df-dif 3922  df-un 3924  df-in 3926 This theorem is referenced by:  dfsymdif3  4254  difun2  4412  diftpsn3  4719  setsfun0  16521  strleun  16593  mreexmrid  16916  mreexexlem2d  16918  mvdco  18575  dprd2da  19166  dmdprdsplit2lem  19169  ablfac1eulem  19196  lbsextlem4  19935  opsrtoslem2  20733  nulmbl2  24149  uniioombllem3  24198  ex-dif  28217  indifundif  30303  imadifxp  30370  fzodif1  30537  cycpmrn  30827  ballotlemfp1  31834  ballotlemgun  31867  onint1  33882  lindsadd  35022  lindsenlbs  35024  poimirlem2  35031  poimirlem6  35035  poimirlem7  35036  poimirlem8  35037  poimirlem22  35051  dvmptfprodlem  42539  fourierdlem102  42803  fourierdlem114  42815  caragenuncllem  43104  carageniuncllem1  43113
 Copyright terms: Public domain W3C validator