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

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.
StepHypRef Expression
1 unopab 5231 . . 3 ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)} ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧𝑧𝐴𝑦)}) = {⟨𝑥, 𝑦⟩ ∣ (∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧𝑧𝐴𝑦))}
2 brun 5200 . . . . . . . 8 (𝑥(𝐵𝐶)𝑧 ↔ (𝑥𝐵𝑧𝑥𝐶𝑧))
32anbi1i 625 . . . . . . 7 ((𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦) ↔ ((𝑥𝐵𝑧𝑥𝐶𝑧) ∧ 𝑧𝐴𝑦))
4 andir 1008 . . . . . . 7 (((𝑥𝐵𝑧𝑥𝐶𝑧) ∧ 𝑧𝐴𝑦) ↔ ((𝑥𝐵𝑧𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧𝑧𝐴𝑦)))
53, 4bitri 275 . . . . . 6 ((𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦) ↔ ((𝑥𝐵𝑧𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧𝑧𝐴𝑦)))
65exbii 1851 . . . . 5 (∃𝑧(𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦) ↔ ∃𝑧((𝑥𝐵𝑧𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧𝑧𝐴𝑦)))
7 19.43 1886 . . . . 5 (∃𝑧((𝑥𝐵𝑧𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧𝑧𝐴𝑦)) ↔ (∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧𝑧𝐴𝑦)))
86, 7bitr2i 276 . . . 4 ((∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧𝑧𝐴𝑦)) ↔ ∃𝑧(𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦))
98opabbii 5216 . . 3 {⟨𝑥, 𝑦⟩ ∣ (∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧𝑧𝐴𝑦))} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦)}
101, 9eqtri 2761 . 2 ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)} ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧𝑧𝐴𝑦)}) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦)}
11 df-co 5686 . . 3 (𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
12 df-co 5686 . . 3 (𝐴𝐶) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧𝑧𝐴𝑦)}
1311, 12uneq12i 4162 . 2 ((𝐴𝐵) ∪ (𝐴𝐶)) = ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)} ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧𝑧𝐴𝑦)})
14 df-co 5686 . 2 (𝐴 ∘ (𝐵𝐶)) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦)}
1510, 13, 143eqtr4ri 2772 1 (𝐴 ∘ (𝐵𝐶)) = ((𝐴𝐵) ∪ (𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wa 397  wo 846   = wceq 1542  wex 1782  cun 3947   class class class wbr 5149  {copab 5211  ccom 5681
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-br 5150  df-opab 5212  df-co 5686
This theorem is referenced by:  f1ofvswap  7304  mvdco  19313  ustssco  23719  coprprop  31921  cycpmconjv  32301  cvmliftlem10  34285  poimirlem9  36497  diophren  41551  rtrclex  42368  trclubgNEW  42369  trclexi  42371  rtrclexi  42372  cnvtrcl0  42377  trrelsuperrel2dg  42422  cotrclrcl  42493  frege131d  42515
  Copyright terms: Public domain W3C validator