Theorem indir 4261

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

Step	Hyp	Ref	Expression
1		indi 4259	. 2 ⊢ (𝐶 ∩ (𝐴 ∪ 𝐵)) = ((𝐶 ∩ 𝐴) ∪ (𝐶 ∩ 𝐵))
2		incom 4184	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = (𝐶 ∩ (𝐴 ∪ 𝐵))
3		incom 4184	. . 3 ⊢ (𝐴 ∩ 𝐶) = (𝐶 ∩ 𝐴)
4		incom 4184	. . 3 ⊢ (𝐵 ∩ 𝐶) = (𝐶 ∩ 𝐵)
5	3, 4	uneq12i 4141	. 2 ⊢ ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶)) = ((𝐶 ∩ 𝐴) ∪ (𝐶 ∩ 𝐵))
6	1, 2, 5	3eqtr4i 2768	1 ⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶))

Syntax hints:   = wceq 1540   ∪ cun 3924   ∩ cin 3925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-un 3931  df-in 3933

This theorem is referenced by:  difundir  4266  undisj1  4437  disjpr2  4689  resundir  5981  predun  6317  djuassen  10193  fin23lem26  10339  fpwwe2lem12  10656  neitr  23118  fiuncmp  23342  connsuba  23358  trfil2  23825  tsmsres  24082  trust  24168  restmetu  24509  volun  25498  uniioombllem3  25538  itgsplitioo  25791  ppiprm  27113  chtprm  27115  chtdif  27120  ppidif  27125  cycpmco2f1  33135  carsgclctunlem1  34349  ballotlemfp1  34524  ballotlemgun  34557  mrsubvrs  35544  mthmpps  35604  fixun  35927  mbfposadd  37691  metakunt17  42234  metakunt21  42238  metakunt22  42239  metakunt24  42241  iunrelexp0  43726  31prm  47611