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

Theorem difindi 4292
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 4277 . . 3 (𝐵𝐶) = (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶)))
21difeq2i 4123 . 2 (𝐴 ∖ (𝐵𝐶)) = (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))))
3 indi 4284 . . 3 (𝐴 ∩ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))) = ((𝐴 ∩ (V ∖ 𝐵)) ∪ (𝐴 ∩ (V ∖ 𝐶)))
4 dfin2 4271 . . 3 (𝐴 ∩ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))) = (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))))
5 invdif 4279 . . . 4 (𝐴 ∩ (V ∖ 𝐵)) = (𝐴𝐵)
6 invdif 4279 . . . 4 (𝐴 ∩ (V ∖ 𝐶)) = (𝐴𝐶)
75, 6uneq12i 4166 . . 3 ((𝐴 ∩ (V ∖ 𝐵)) ∪ (𝐴 ∩ (V ∖ 𝐶))) = ((𝐴𝐵) ∪ (𝐴𝐶))
83, 4, 73eqtr3i 2773 . 2 (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶)))) = ((𝐴𝐵) ∪ (𝐴𝐶))
92, 8eqtri 2765 1 (𝐴 ∖ (𝐵𝐶)) = ((𝐴𝐵) ∪ (𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  Vcvv 3480  cdif 3948  cun 3949  cin 3950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958
This theorem is referenced by:  difdif2  4296  indm  4298  fndifnfp  7196  dprddisj2  20059  fctop  23011  cctop  23013  mretopd  23100  restcld  23180  cfinfil  23901  csdfil  23902  indifundif  32543  difres  32613  unelcarsg  34314  clsk3nimkb  44053  ntrclskb  44082  ntrclsk3  44083  ntrclsk13  44084  salincl  46339  iscnrm3rlem1  48837
  Copyright terms: Public domain W3C validator