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

Theorem difindi 4282
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 4267 . . 3 (𝐵𝐶) = (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶)))
21difeq2i 4120 . 2 (𝐴 ∖ (𝐵𝐶)) = (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))))
3 indi 4274 . . 3 (𝐴 ∩ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))) = ((𝐴 ∩ (V ∖ 𝐵)) ∪ (𝐴 ∩ (V ∖ 𝐶)))
4 dfin2 4261 . . 3 (𝐴 ∩ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))) = (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))))
5 invdif 4269 . . . 4 (𝐴 ∩ (V ∖ 𝐵)) = (𝐴𝐵)
6 invdif 4269 . . . 4 (𝐴 ∩ (V ∖ 𝐶)) = (𝐴𝐶)
75, 6uneq12i 4162 . . 3 ((𝐴 ∩ (V ∖ 𝐵)) ∪ (𝐴 ∩ (V ∖ 𝐶))) = ((𝐴𝐵) ∪ (𝐴𝐶))
83, 4, 73eqtr3i 2769 . 2 (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶)))) = ((𝐴𝐵) ∪ (𝐴𝐶))
92, 8eqtri 2761 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:  difdif2  4287  indm  4289  fndifnfp  7174  dprddisj2  19909  fctop  22507  cctop  22509  mretopd  22596  restcld  22676  cfinfil  23397  csdfil  23398  indifundif  31762  difres  31831  unelcarsg  33311  clsk3nimkb  42791  ntrclskb  42820  ntrclsk3  42821  ntrclsk13  42822  salincl  45040  iscnrm3rlem1  47573
  Copyright terms: Public domain W3C validator