Metamath Proof Explorer

Theorem coundir

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

Ref Expression
Assertion coundir ⊢A∪B∘C=A∘C∪B∘C

Proof

Step Hyp Ref Expression
1 unopab ⊢xz|∃yxCy∧yAz∪xz|∃yxCy∧yBz=xz|∃yxCy∧yAz∨∃yxCy∧yBz
2 brun ⊢yA∪Bz↔yAz∨yBz
3 2 anbi2i ⊢xCy∧yA∪Bz↔xCy∧yAz∨yBz
4 andi ⊢xCy∧yAz∨yBz↔xCy∧yAz∨xCy∧yBz
5 3 4 bitri ⊢xCy∧yA∪Bz↔xCy∧yAz∨xCy∧yBz
6 5 exbii ⊢∃yxCy∧yA∪Bz↔∃yxCy∧yAz∨xCy∧yBz
7 19.43 ⊢∃yxCy∧yAz∨xCy∧yBz↔∃yxCy∧yAz∨∃yxCy∧yBz
8 6 7 bitr2i ⊢∃yxCy∧yAz∨∃yxCy∧yBz↔∃yxCy∧yA∪Bz
9 8 opabbii ⊢xz|∃yxCy∧yAz∨∃yxCy∧yBz=xz|∃yxCy∧yA∪Bz
10 1 9 eqtri ⊢xz|∃yxCy∧yAz∪xz|∃yxCy∧yBz=xz|∃yxCy∧yA∪Bz
11 df-co ⊢A∘C=xz|∃yxCy∧yAz
12 df-co ⊢B∘C=xz|∃yxCy∧yBz
13 11 12 uneq12i ⊢A∘C∪B∘C=xz|∃yxCy∧yAz∪xz|∃yxCy∧yBz
14 df-co ⊢A∪B∘C=xz|∃yxCy∧yA∪Bz
15 10 13 14 3eqtr4ri ⊢A∪B∘C=A∘C∪B∘C