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

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

Proof of Theorem difundir
StepHypRef Expression
1 indir 4292 . 2 ((𝐴𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶)))
2 invdif 4285 . 2 ((𝐴𝐵) ∩ (V ∖ 𝐶)) = ((𝐴𝐵) ∖ 𝐶)
3 invdif 4285 . . 3 (𝐴 ∩ (V ∖ 𝐶)) = (𝐴𝐶)
4 invdif 4285 . . 3 (𝐵 ∩ (V ∖ 𝐶)) = (𝐵𝐶)
53, 4uneq12i 4176 . 2 ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴𝐶) ∪ (𝐵𝐶))
61, 2, 53eqtr3i 2771 1 ((𝐴𝐵) ∖ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537  Vcvv 3478  cdif 3960  cun 3961  cin 3962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970
This theorem is referenced by:  dfsymdif3  4312  difun2  4487  diftpsn3  4807  strleun  17191  setsfun0  17206  mreexmrid  17688  mreexexlem2d  17690  mvdco  19478  dprd2da  20077  dmdprdsplit2lem  20080  ablfac1eulem  20107  lbsextlem4  21181  opsrtoslem2  22098  nulmbl2  25585  uniioombllem3  25634  sltlpss  27960  slelss  27961  ex-dif  30452  indifundif  32552  imadifxp  32621  fzodif1  32801  cycpmrn  33146  ballotlemfp1  34473  ballotlemgun  34506  onint1  36432  lindsadd  37600  lindsenlbs  37602  poimirlem2  37609  poimirlem6  37613  poimirlem7  37614  poimirlem8  37615  poimirlem22  37629  dvmptfprodlem  45900  fourierdlem102  46164  fourierdlem114  46176  caragenuncllem  46468  carageniuncllem1  46477
  Copyright terms: Public domain W3C validator