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

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

Proof of Theorem difundir
StepHypRef Expression
1 indir 4018 . 2 ((𝐴𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶)))
2 invdif 4011 . 2 ((𝐴𝐵) ∩ (V ∖ 𝐶)) = ((𝐴𝐵) ∖ 𝐶)
3 invdif 4011 . . 3 (𝐴 ∩ (V ∖ 𝐶)) = (𝐴𝐶)
4 invdif 4011 . . 3 (𝐵 ∩ (V ∖ 𝐶)) = (𝐵𝐶)
53, 4uneq12i 3908 . 2 ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴𝐶) ∪ (𝐵𝐶))
61, 2, 53eqtr3i 2790 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:  dfsymdif3  4036  difun2  4192  diftpsn3  4477  diftpsn3OLD  4478  setsfun0  16096  strleun  16174  mreexmrid  16505  mreexexlem2d  16507  mvdco  18065  dprd2da  18641  dmdprdsplit2lem  18644  ablfac1eulem  18671  lbsextlem4  19363  opsrtoslem2  19687  nulmbl2  23504  uniioombllem3  23553  ex-dif  27591  indifundif  29663  imadifxp  29721  ballotlemfp1  30862  ballotlemgun  30895  onint1  32754  lindsenlbs  33717  poimirlem2  33724  poimirlem6  33728  poimirlem7  33729  poimirlem8  33730  poimirlem22  33744  dvmptfprodlem  40662  fourierdlem102  40928  fourierdlem114  40940  caragenuncllem  41232  carageniuncllem1  41241
  Copyright terms: Public domain W3C validator