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

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

Proof of Theorem difundir
StepHypRef Expression
1 indir 4276 . 2 ((𝐴𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶)))
2 invdif 4269 . 2 ((𝐴𝐵) ∩ (V ∖ 𝐶)) = ((𝐴𝐵) ∖ 𝐶)
3 invdif 4269 . . 3 (𝐴 ∩ (V ∖ 𝐶)) = (𝐴𝐶)
4 invdif 4269 . . 3 (𝐵 ∩ (V ∖ 𝐶)) = (𝐵𝐶)
53, 4uneq12i 4162 . 2 ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴𝐶) ∪ (𝐵𝐶))
61, 2, 53eqtr3i 2769 1 ((𝐴𝐵) ∖ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  Vcvv 3475  cdif 3946  cun 3947  cin 3948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956
This theorem is referenced by:  dfsymdif3  4297  difun2  4481  diftpsn3  4806  strleun  17090  setsfun0  17105  mreexmrid  17587  mreexexlem2d  17589  mvdco  19313  dprd2da  19912  dmdprdsplit2lem  19915  ablfac1eulem  19942  lbsextlem4  20774  opsrtoslem2  21617  nulmbl2  25053  uniioombllem3  25102  sltlpss  27401  ex-dif  29676  indifundif  31762  imadifxp  31832  fzodif1  32004  cycpmrn  32302  ballotlemfp1  33490  ballotlemgun  33523  onint1  35334  lindsadd  36481  lindsenlbs  36483  poimirlem2  36490  poimirlem6  36494  poimirlem7  36495  poimirlem8  36496  poimirlem22  36510  dvmptfprodlem  44660  fourierdlem102  44924  fourierdlem114  44936  caragenuncllem  45228  carageniuncllem1  45237
  Copyright terms: Public domain W3C validator