Theorem coundi 6247

Description: Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

Assertion

Ref	Expression
coundi	⊢ (𝐴 ∘ (𝐵 ∪ 𝐶)) = ((𝐴 ∘ 𝐵) ∪ (𝐴 ∘ 𝐶))

Proof of Theorem coundi

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		unopab 5189	. . 3 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)}) = {⟨𝑥, 𝑦⟩ ∣ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦))}
2		brun 5160	. . . . . . . 8 ⊢ (𝑥(𝐵 ∪ 𝐶)𝑧 ↔ (𝑥𝐵𝑧 ∨ 𝑥𝐶𝑧))
3	2	anbi1i 636	. . . . . . 7 ⊢ ((𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦) ↔ ((𝑥𝐵𝑧 ∨ 𝑥𝐶𝑧) ∧ 𝑧𝐴𝑦))
4		andir 1026	. . . . . . 7 ⊢ (((𝑥𝐵𝑧 ∨ 𝑥𝐶𝑧) ∧ 𝑧𝐴𝑦) ↔ ((𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)))
5	3, 4	bitri 278	. . . . . 6 ⊢ ((𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦) ↔ ((𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)))
6	5	exbii 1881	. . . . 5 ⊢ (∃𝑧(𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦) ↔ ∃𝑧((𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)))
7		19.43 1915	. . . . 5 ⊢ (∃𝑧((𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)) ↔ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)))
8	6, 7	bitr2i 279	. . . 4 ⊢ ((∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)) ↔ ∃𝑧(𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦))
9	8	opabbii 5176	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦))} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦)}
10	1, 9	eqtri 2785	. 2 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)}) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦)}
11		df-co 5668	. . 3 ⊢ (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)}
12		df-co 5668	. . 3 ⊢ (𝐴 ∘ 𝐶) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)}
13	11, 12	uneq12i 4116	. 2 ⊢ ((𝐴 ∘ 𝐵) ∪ (𝐴 ∘ 𝐶)) = ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)})
14		df-co 5668	. 2 ⊢ (𝐴 ∘ (𝐵 ∪ 𝐶)) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦)}
15	10, 13, 14	3eqtr4ri 2796	1 ⊢ (𝐴 ∘ (𝐵 ∪ 𝐶)) = ((𝐴 ∘ 𝐵) ∪ (𝐴 ∘ 𝐶))

This proof depends on syntax axioms:   ∧ wa 401   ∨ wo 861   = wceq 1570  ∃wex 1812   ∪ cun 3900   class class class wbr 5107  {copab 5171   ∘ ccom 5663

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-br 5108  df-opab 5172  df-co 5668

This theorem is used by:  f1ofvswap  7311  mvdco  19578  ustssco  24447  coprprop  33179  cycpmconjv  33590  cvmliftlem10  35881  poimirlem9  38386  diophren  43662  rtrclex  44465  trclubgNEW  44466  trclexi  44468  rtrclexi  44469  cnvtrcl0  44474  trrelsuperrel2dg  44519  cotrclrcl  44590  frege131d  44612  dftpos6  49809