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

Theorem difindi 4024
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 4009 . . 3 (𝐵𝐶) = (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶)))
21difeq2i 3868 . 2 (𝐴 ∖ (𝐵𝐶)) = (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))))
3 indi 4016 . . 3 (𝐴 ∩ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))) = ((𝐴 ∩ (V ∖ 𝐵)) ∪ (𝐴 ∩ (V ∖ 𝐶)))
4 dfin2 4003 . . 3 (𝐴 ∩ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))) = (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶))))
5 invdif 4011 . . . 4 (𝐴 ∩ (V ∖ 𝐵)) = (𝐴𝐵)
6 invdif 4011 . . . 4 (𝐴 ∩ (V ∖ 𝐶)) = (𝐴𝐶)
75, 6uneq12i 3908 . . 3 ((𝐴 ∩ (V ∖ 𝐵)) ∪ (𝐴 ∩ (V ∖ 𝐶))) = ((𝐴𝐵) ∪ (𝐴𝐶))
83, 4, 73eqtr3i 2790 . 2 (𝐴 ∖ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐶)))) = ((𝐴𝐵) ∪ (𝐴𝐶))
92, 8eqtri 2782 1 (𝐴 ∖ (𝐵𝐶)) = ((𝐴𝐵) ∪ (𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  Vcvv 3340  cdif 3712  cun 3713  cin 3714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722
This theorem is referenced by:  difdif2  4027  indm  4029  fndifnfp  6607  dprddisj2  18658  fctop  21030  cctop  21032  mretopd  21118  restcld  21198  cfinfil  21918  csdfil  21919  indifundif  29684  difres  29741  unelcarsg  30704  clsk3nimkb  38858  ntrclskb  38887  ntrclsk3  38888  ntrclsk13  38889  salincl  41064
  Copyright terms: Public domain W3C validator