Step | Hyp | Ref
| Expression |
1 | | unopab 4638 |
. . 3
⊢ ({〈x, z〉 ∣ ∃y(xCy ∧ yAz)} ∪
{〈x,
z〉 ∣ ∃y(xCy ∧ yBz)}) = {〈x, z〉 ∣ (∃y(xCy ∧ yAz) ∨ ∃y(xCy ∧ yBz))} |
2 | | brun 4692 |
. . . . . . . 8
⊢ (y(A ∪
B)z
↔ (yAz ∨ yBz)) |
3 | 2 | anbi2i 675 |
. . . . . . 7
⊢ ((xCy ∧ y(A ∪
B)z)
↔ (xCy ∧ (yAz ∨ yBz))) |
4 | | andi 837 |
. . . . . . 7
⊢ ((xCy ∧ (yAz ∨ yBz)) ↔ ((xCy ∧ yAz) ∨ (xCy ∧ yBz))) |
5 | 3, 4 | bitri 240 |
. . . . . 6
⊢ ((xCy ∧ y(A ∪
B)z)
↔ ((xCy ∧ yAz) ∨ (xCy ∧ yBz))) |
6 | 5 | exbii 1582 |
. . . . 5
⊢ (∃y(xCy ∧ y(A ∪
B)z)
↔ ∃y((xCy ∧ yAz) ∨ (xCy ∧ yBz))) |
7 | | 19.43 1605 |
. . . . 5
⊢ (∃y((xCy ∧ yAz) ∨ (xCy ∧ yBz)) ↔ (∃y(xCy ∧ yAz) ∨ ∃y(xCy ∧ yBz))) |
8 | 6, 7 | bitr2i 241 |
. . . 4
⊢ ((∃y(xCy ∧ yAz) ∨ ∃y(xCy ∧ yBz)) ↔ ∃y(xCy ∧ y(A ∪
B)z)) |
9 | 8 | opabbii 4626 |
. . 3
⊢ {〈x, z〉 ∣ (∃y(xCy ∧ yAz) ∨ ∃y(xCy ∧ yBz))} = {〈x, z〉 ∣ ∃y(xCy ∧ y(A ∪ B)z)} |
10 | 1, 9 | eqtri 2373 |
. 2
⊢ ({〈x, z〉 ∣ ∃y(xCy ∧ yAz)} ∪
{〈x,
z〉 ∣ ∃y(xCy ∧ yBz)}) = {〈x, z〉 ∣ ∃y(xCy ∧ y(A ∪ B)z)} |
11 | | df-co 4726 |
. . 3
⊢ (A ∘ C) = {〈x, z〉 ∣ ∃y(xCy ∧ yAz)} |
12 | | df-co 4726 |
. . 3
⊢ (B ∘ C) = {〈x, z〉 ∣ ∃y(xCy ∧ yBz)} |
13 | 11, 12 | uneq12i 3416 |
. 2
⊢ ((A ∘ C) ∪ (B
∘ C)) =
({〈x,
z〉 ∣ ∃y(xCy ∧ yAz)} ∪
{〈x,
z〉 ∣ ∃y(xCy ∧ yBz)}) |
14 | | df-co 4726 |
. 2
⊢ ((A ∪ B) ∘ C) = {〈x, z〉 ∣ ∃y(xCy ∧ y(A ∪ B)z)} |
15 | 10, 13, 14 | 3eqtr4ri 2384 |
1
⊢ ((A ∪ B) ∘ C) =
((A ∘
C) ∪ (B ∘ C)) |