Step | Hyp | Ref
| Expression |
1 | | 19.43 1516 |
. . . 4
⊢ (∃y((x ∈ y ∧ y = A) ∨ (x ∈ y ∧ y = B)) ↔ (∃y(x ∈ y ∧ y = A) ∨ ∃y(x ∈ y ∧ y = B))) |
2 | | vex 2554 |
. . . . . . . 8
⊢ y ∈
V |
3 | 2 | elpr 3385 |
. . . . . . 7
⊢ (y ∈ {A, B} ↔
(y = A
∨ y =
B)) |
4 | 3 | anbi2i 430 |
. . . . . 6
⊢
((x ∈ y ∧ y ∈ {A, B}) ↔ (x
∈ y ∧ (y = A ∨ y = B))) |
5 | | andi 730 |
. . . . . 6
⊢
((x ∈ y ∧ (y = A ∨ y = B)) ↔
((x ∈
y ∧
y = A)
∨ (x ∈ y ∧ y = B))) |
6 | 4, 5 | bitri 173 |
. . . . 5
⊢
((x ∈ y ∧ y ∈ {A, B}) ↔ ((x
∈ y ∧ y = A) ∨ (x ∈ y ∧ y = B))) |
7 | 6 | exbii 1493 |
. . . 4
⊢ (∃y(x ∈ y ∧ y ∈ {A, B}) ↔
∃y((x ∈ y ∧ y = A) ∨ (x ∈ y ∧ y = B))) |
8 | | unipr.1 |
. . . . . . 7
⊢ A ∈
V |
9 | 8 | clel3 2673 |
. . . . . 6
⊢ (x ∈ A ↔ ∃y(y = A ∧ x ∈ y)) |
10 | | exancom 1496 |
. . . . . 6
⊢ (∃y(y = A ∧ x ∈ y) ↔
∃y(x ∈ y ∧ y = A)) |
11 | 9, 10 | bitri 173 |
. . . . 5
⊢ (x ∈ A ↔ ∃y(x ∈ y ∧ y = A)) |
12 | | unipr.2 |
. . . . . . 7
⊢ B ∈
V |
13 | 12 | clel3 2673 |
. . . . . 6
⊢ (x ∈ B ↔ ∃y(y = B ∧ x ∈ y)) |
14 | | exancom 1496 |
. . . . . 6
⊢ (∃y(y = B ∧ x ∈ y) ↔
∃y(x ∈ y ∧ y = B)) |
15 | 13, 14 | bitri 173 |
. . . . 5
⊢ (x ∈ B ↔ ∃y(x ∈ y ∧ y = B)) |
16 | 11, 15 | orbi12i 680 |
. . . 4
⊢
((x ∈ A ∨ x ∈ B) ↔
(∃y(x ∈ y ∧ y = A) ∨ ∃y(x ∈ y ∧ y = B))) |
17 | 1, 7, 16 | 3bitr4ri 202 |
. . 3
⊢
((x ∈ A ∨ x ∈ B) ↔
∃y(x ∈ y ∧ y ∈ {A, B})) |
18 | 17 | abbii 2150 |
. 2
⊢ {x ∣ (x
∈ A ∨ x ∈ B)} =
{x ∣ ∃y(x ∈ y ∧ y ∈ {A, B})} |
19 | | df-un 2916 |
. 2
⊢ (A ∪ B) =
{x ∣ (x ∈ A ∨ x ∈ B)} |
20 | | df-uni 3572 |
. 2
⊢ ∪ {A, B} = {x ∣
∃y(x ∈ y ∧ y ∈ {A, B})} |
21 | 18, 19, 20 | 3eqtr4ri 2068 |
1
⊢ ∪ {A, B} = (A ∪
B) |