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

Theorem difindi 4255
Description: Distributive law for class difference. Theorem 40 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
Assertion
Ref Expression
difindi (𝐴 ∖ (𝐵𝐶)) = ((𝐴𝐵) ∪ (𝐴𝐶))

Proof of Theorem difindi
StepHypRef Expression
1 dfin3 4240 . . 3 (𝐵𝐶) = (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶)))
21difeq2i 4093 . 2 (𝐴 ∖ (𝐵𝐶)) = (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))))
3 indi 4247 . . 3 (𝐴 ∩ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))) = ((𝐴 ∩ (V ∖ 𝐵)) ∪ (𝐴 ∩ (V ∖ 𝐶)))
4 dfin2 4234 . . 3 (𝐴 ∩ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))) = (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))))
5 invdif 4242 . . . 4 (𝐴 ∩ (V ∖ 𝐵)) = (𝐴𝐵)
6 invdif 4242 . . . 4 (𝐴 ∩ (V ∖ 𝐶)) = (𝐴𝐶)
75, 6uneq12i 4134 . . 3 ((𝐴 ∩ (V ∖ 𝐵)) ∪ (𝐴 ∩ (V ∖ 𝐶))) = ((𝐴𝐵) ∪ (𝐴𝐶))
83, 4, 73eqtr3i 2849 . 2 (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶)))) = ((𝐴𝐵) ∪ (𝐴𝐶))
92, 8eqtri 2841 1 (𝐴 ∖ (𝐵𝐶)) = ((𝐴𝐵) ∪ (𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  Vcvv 3492  cdif 3930  cun 3931  cin 3932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940
This theorem is referenced by:  difdif2  4258  indm  4260  fndifnfp  6930  dprddisj2  19090  fctop  21540  cctop  21542  mretopd  21628  restcld  21708  cfinfil  22429  csdfil  22430  indifundif  30212  difres  30278  unelcarsg  31469  clsk3nimkb  40268  ntrclskb  40297  ntrclsk3  40298  ntrclsk13  40299  salincl  42485
  Copyright terms: Public domain W3C validator