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

Theorem coundi 6078
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.
StepHypRef Expression
1 unopab 5121 . . 3 ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)} ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧𝑧𝐴𝑦)}) = {⟨𝑥, 𝑦⟩ ∣ (∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧𝑧𝐴𝑦))}
2 brun 5093 . . . . . . . 8 (𝑥(𝐵𝐶)𝑧 ↔ (𝑥𝐵𝑧𝑥𝐶𝑧))
32anbi1i 626 . . . . . . 7 ((𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦) ↔ ((𝑥𝐵𝑧𝑥𝐶𝑧) ∧ 𝑧𝐴𝑦))
4 andir 1006 . . . . . . 7 (((𝑥𝐵𝑧𝑥𝐶𝑧) ∧ 𝑧𝐴𝑦) ↔ ((𝑥𝐵𝑧𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧𝑧𝐴𝑦)))
53, 4bitri 278 . . . . . 6 ((𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦) ↔ ((𝑥𝐵𝑧𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧𝑧𝐴𝑦)))
65exbii 1849 . . . . 5 (∃𝑧(𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦) ↔ ∃𝑧((𝑥𝐵𝑧𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧𝑧𝐴𝑦)))
7 19.43 1883 . . . . 5 (∃𝑧((𝑥𝐵𝑧𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧𝑧𝐴𝑦)) ↔ (∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧𝑧𝐴𝑦)))
86, 7bitr2i 279 . . . 4 ((∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧𝑧𝐴𝑦)) ↔ ∃𝑧(𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦))
98opabbii 5109 . . 3 {⟨𝑥, 𝑦⟩ ∣ (∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧𝑧𝐴𝑦))} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦)}
101, 9eqtri 2845 . 2 ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)} ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧𝑧𝐴𝑦)}) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦)}
11 df-co 5541 . . 3 (𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
12 df-co 5541 . . 3 (𝐴𝐶) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧𝑧𝐴𝑦)}
1311, 12uneq12i 4112 . 2 ((𝐴𝐵) ∪ (𝐴𝐶)) = ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)} ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧𝑧𝐴𝑦)})
14 df-co 5541 . 2 (𝐴 ∘ (𝐵𝐶)) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦)}
1510, 13, 143eqtr4ri 2856 1 (𝐴 ∘ (𝐵𝐶)) = ((𝐴𝐵) ∪ (𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wa 399  wo 844   = wceq 1538  wex 1781  cun 3906   class class class wbr 5042  {copab 5104  ccom 5536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-12 2178  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-v 3471  df-un 3913  df-br 5043  df-opab 5105  df-co 5541
This theorem is referenced by:  mvdco  18564  ustssco  22818  coprprop  30443  cycpmconjv  30815  cvmliftlem10  32615  poimirlem9  35025  diophren  39685  rtrclex  40248  trclubgNEW  40249  trclexi  40251  rtrclexi  40252  cnvtrcl0  40257  trrelsuperrel2dg  40303  cotrclrcl  40374  frege131d  40396
  Copyright terms: Public domain W3C validator