MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  indir Unicode version

Theorem indir 3712
Description: Distributive law for intersection over union. Theorem 28 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.)
Assertion
Ref Expression
indir

Proof of Theorem indir
StepHypRef Expression
1 indi 3710 . 2
2 incom 3657 . 2
3 incom 3657 . . 3
4 incom 3657 . . 3
53, 4uneq12i 3622 . 2
61, 2, 53eqtr4i 2493 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1370  u.cun 3440  i^icin 3441
This theorem is referenced by:  difundir  3717  undisj1  3844  disjpr2  4055  resundir  5242  cdaassen  8488  fin23lem26  8631  fpwwe2lem13  8946  neitr  19183  fiuncmp  19406  consuba  19423  trfil2  19859  tsmsresOLD  20116  tsmsres  20117  trust  20203  restmetu  20561  volun  21426  uniioombllem3  21465  itgsplitioo  21715  ppiprm  22889  chtprm  22891  chtdif  22896  ppidif  22901  ballotlemfp1  27330  ballotlemgun  27363  predun  28107  fixun  28396  mbfposadd  28899
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3083  df-un 3447  df-in 3449
  Copyright terms: Public domain W3C validator