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  16116  strleun  16194  mreexmrid  16525  mreexexlem2d  16527  mvdco  18085  dprd2da  18661  dmdprdsplit2lem  18664  ablfac1eulem  18691  lbsextlem4  19383  opsrtoslem2  19707  nulmbl2  23524  uniioombllem3  23573  ex-dif  27612  indifundif  29684  imadifxp  29742  ballotlemfp1  30883  ballotlemgun  30916  onint1  32775  lindsenlbs  33735  poimirlem2  33742  poimirlem6  33746  poimirlem7  33747  poimirlem8  33748  poimirlem22  33762  dvmptfprodlem  40680  fourierdlem102  40946  fourierdlem114  40958  caragenuncllem  41250  carageniuncllem1  41259
  Copyright terms: Public domain W3C validator