Step | Hyp | Ref
| Expression |
1 | | unopab 3827 |
. . 3
⊢
({〈x, y〉 ∣ ∃z(xBz ∧ zAy)} ∪ {〈x, y〉
∣ ∃z(x𝐶z ∧ zAy)}) = {〈x,
y〉 ∣ (∃z(xBz ∧ zAy) ∨ ∃z(x𝐶z ∧ zAy))} |
2 | | brun 3801 |
. . . . . . . 8
⊢ (x(B ∪ 𝐶)z ↔ (xBz ∨ x𝐶z)) |
3 | 2 | anbi1i 431 |
. . . . . . 7
⊢
((x(B ∪ 𝐶)z ∧ zAy) ↔
((xBz ∨ x𝐶z) ∧ zAy)) |
4 | | andir 731 |
. . . . . . 7
⊢
(((xBz ∨ x𝐶z) ∧ zAy) ↔ ((xBz ∧ zAy) ∨ (x𝐶z ∧ zAy))) |
5 | 3, 4 | bitri 173 |
. . . . . 6
⊢
((x(B ∪ 𝐶)z ∧ zAy) ↔
((xBz ∧ zAy) ∨ (x𝐶z ∧ zAy))) |
6 | 5 | exbii 1493 |
. . . . 5
⊢ (∃z(x(B ∪ 𝐶)z ∧ zAy) ↔ ∃z((xBz ∧ zAy) ∨ (x𝐶z ∧ zAy))) |
7 | | 19.43 1516 |
. . . . 5
⊢ (∃z((xBz ∧ zAy) ∨ (x𝐶z ∧ zAy)) ↔
(∃z(xBz ∧ zAy) ∨ ∃z(x𝐶z ∧ zAy))) |
8 | 6, 7 | bitr2i 174 |
. . . 4
⊢ ((∃z(xBz ∧ zAy) ∨ ∃z(x𝐶z ∧ zAy)) ↔
∃z(x(B ∪ 𝐶)z ∧ zAy)) |
9 | 8 | opabbii 3815 |
. . 3
⊢
{〈x, y〉 ∣ (∃z(xBz ∧ zAy) ∨ ∃z(x𝐶z ∧ zAy))} =
{〈x, y〉 ∣ ∃z(x(B ∪ 𝐶)z ∧ zAy)} |
10 | 1, 9 | eqtri 2057 |
. 2
⊢
({〈x, y〉 ∣ ∃z(xBz ∧ zAy)} ∪ {〈x, y〉
∣ ∃z(x𝐶z ∧ zAy)}) = {〈x,
y〉 ∣ ∃z(x(B ∪ 𝐶)z ∧ zAy)} |
11 | | df-co 4297 |
. . 3
⊢ (A ∘ B) =
{〈x, y〉 ∣ ∃z(xBz ∧ zAy)} |
12 | | df-co 4297 |
. . 3
⊢ (A ∘ 𝐶) = {〈x, y〉
∣ ∃z(x𝐶z ∧ zAy)} |
13 | 11, 12 | uneq12i 3089 |
. 2
⊢
((A ∘ B) ∪ (A
∘ 𝐶)) =
({〈x, y〉 ∣ ∃z(xBz ∧ zAy)} ∪ {〈x, y〉
∣ ∃z(x𝐶z ∧ zAy)}) |
14 | | df-co 4297 |
. 2
⊢ (A ∘ (B
∪ 𝐶)) = {〈x, y〉
∣ ∃z(x(B ∪ 𝐶)z ∧ zAy)} |
15 | 10, 13, 14 | 3eqtr4ri 2068 |
1
⊢ (A ∘ (B
∪ 𝐶)) = ((A ∘ B)
∪ (A ∘ 𝐶)) |