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

Theorem coundi 6269
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 5230 . . 3 ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)} ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧𝑧𝐴𝑦)}) = {⟨𝑥, 𝑦⟩ ∣ (∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧𝑧𝐴𝑦))}
2 brun 5199 . . . . . . . 8 (𝑥(𝐵𝐶)𝑧 ↔ (𝑥𝐵𝑧𝑥𝐶𝑧))
32anbi1i 624 . . . . . . 7 ((𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦) ↔ ((𝑥𝐵𝑧𝑥𝐶𝑧) ∧ 𝑧𝐴𝑦))
4 andir 1010 . . . . . . 7 (((𝑥𝐵𝑧𝑥𝐶𝑧) ∧ 𝑧𝐴𝑦) ↔ ((𝑥𝐵𝑧𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧𝑧𝐴𝑦)))
53, 4bitri 275 . . . . . 6 ((𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦) ↔ ((𝑥𝐵𝑧𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧𝑧𝐴𝑦)))
65exbii 1845 . . . . 5 (∃𝑧(𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦) ↔ ∃𝑧((𝑥𝐵𝑧𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧𝑧𝐴𝑦)))
7 19.43 1880 . . . . 5 (∃𝑧((𝑥𝐵𝑧𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧𝑧𝐴𝑦)) ↔ (∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧𝑧𝐴𝑦)))
86, 7bitr2i 276 . . . 4 ((∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧𝑧𝐴𝑦)) ↔ ∃𝑧(𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦))
98opabbii 5215 . . 3 {⟨𝑥, 𝑦⟩ ∣ (∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧𝑧𝐴𝑦))} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦)}
101, 9eqtri 2763 . 2 ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)} ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧𝑧𝐴𝑦)}) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦)}
11 df-co 5698 . . 3 (𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
12 df-co 5698 . . 3 (𝐴𝐶) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧𝑧𝐴𝑦)}
1311, 12uneq12i 4176 . 2 ((𝐴𝐵) ∪ (𝐴𝐶)) = ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)} ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧𝑧𝐴𝑦)})
14 df-co 5698 . 2 (𝐴 ∘ (𝐵𝐶)) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦)}
1510, 13, 143eqtr4ri 2774 1 (𝐴 ∘ (𝐵𝐶)) = ((𝐴𝐵) ∪ (𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wa 395  wo 847   = wceq 1537  wex 1776  cun 3961   class class class wbr 5148  {copab 5210  ccom 5693
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-br 5149  df-opab 5211  df-co 5698
This theorem is referenced by:  f1ofvswap  7326  mvdco  19478  ustssco  24239  coprprop  32714  cycpmconjv  33145  cvmliftlem10  35279  poimirlem9  37616  diophren  42801  rtrclex  43607  trclubgNEW  43608  trclexi  43610  rtrclexi  43611  cnvtrcl0  43616  trrelsuperrel2dg  43661  cotrclrcl  43732  frege131d  43754
  Copyright terms: Public domain W3C validator