| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | unopab 5223 | . . 3
⊢
({〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧)} ∪ {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧)}) = {〈𝑥, 𝑧〉 ∣ (∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧) ∨ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧))} | 
| 2 |  | brun 5193 | . . . . . . . 8
⊢ (𝑦(𝐴 ∪ 𝐵)𝑧 ↔ (𝑦𝐴𝑧 ∨ 𝑦𝐵𝑧)) | 
| 3 | 2 | anbi2i 623 | . . . . . . 7
⊢ ((𝑥𝐶𝑦 ∧ 𝑦(𝐴 ∪ 𝐵)𝑧) ↔ (𝑥𝐶𝑦 ∧ (𝑦𝐴𝑧 ∨ 𝑦𝐵𝑧))) | 
| 4 |  | andi 1009 | . . . . . . 7
⊢ ((𝑥𝐶𝑦 ∧ (𝑦𝐴𝑧 ∨ 𝑦𝐵𝑧)) ↔ ((𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧) ∨ (𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧))) | 
| 5 | 3, 4 | bitri 275 | . . . . . 6
⊢ ((𝑥𝐶𝑦 ∧ 𝑦(𝐴 ∪ 𝐵)𝑧) ↔ ((𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧) ∨ (𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧))) | 
| 6 | 5 | exbii 1847 | . . . . 5
⊢
(∃𝑦(𝑥𝐶𝑦 ∧ 𝑦(𝐴 ∪ 𝐵)𝑧) ↔ ∃𝑦((𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧) ∨ (𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧))) | 
| 7 |  | 19.43 1881 | . . . . 5
⊢
(∃𝑦((𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧) ∨ (𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧)) ↔ (∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧) ∨ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧))) | 
| 8 | 6, 7 | bitr2i 276 | . . . 4
⊢
((∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧) ∨ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧)) ↔ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦(𝐴 ∪ 𝐵)𝑧)) | 
| 9 | 8 | opabbii 5209 | . . 3
⊢
{〈𝑥, 𝑧〉 ∣ (∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧) ∨ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧))} = {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦(𝐴 ∪ 𝐵)𝑧)} | 
| 10 | 1, 9 | eqtri 2764 | . 2
⊢
({〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧)} ∪ {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧)}) = {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦(𝐴 ∪ 𝐵)𝑧)} | 
| 11 |  | df-co 5693 | . . 3
⊢ (𝐴 ∘ 𝐶) = {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧)} | 
| 12 |  | df-co 5693 | . . 3
⊢ (𝐵 ∘ 𝐶) = {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧)} | 
| 13 | 11, 12 | uneq12i 4165 | . 2
⊢ ((𝐴 ∘ 𝐶) ∪ (𝐵 ∘ 𝐶)) = ({〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧)} ∪ {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧)}) | 
| 14 |  | df-co 5693 | . 2
⊢ ((𝐴 ∪ 𝐵) ∘ 𝐶) = {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦(𝐴 ∪ 𝐵)𝑧)} | 
| 15 | 10, 13, 14 | 3eqtr4ri 2775 | 1
⊢ ((𝐴 ∪ 𝐵) ∘ 𝐶) = ((𝐴 ∘ 𝐶) ∪ (𝐵 ∘ 𝐶)) |