Step | Hyp | Ref
| Expression |
1 | | eluni 3894 |
. . 3
⊢ (x ∈ ∪℘1A ↔ ∃y(x ∈ y ∧ y ∈ ℘1A)) |
2 | | elpw1 4144 |
. . . . . 6
⊢ (y ∈ ℘1A ↔ ∃z ∈ A y = {z}) |
3 | 2 | anbi1i 676 |
. . . . 5
⊢ ((y ∈ ℘1A ∧ x ∈ y) ↔ (∃z ∈ A y = {z} ∧ x ∈ y)) |
4 | | ancom 437 |
. . . . 5
⊢ ((x ∈ y ∧ y ∈ ℘1A) ↔ (y
∈ ℘1A ∧ x ∈ y)) |
5 | | r19.41v 2764 |
. . . . 5
⊢ (∃z ∈ A (y = {z} ∧ x ∈ y) ↔
(∃z
∈ A
y = {z}
∧ x ∈ y)) |
6 | 3, 4, 5 | 3bitr4i 268 |
. . . 4
⊢ ((x ∈ y ∧ y ∈ ℘1A) ↔ ∃z ∈ A (y = {z} ∧ x ∈ y)) |
7 | 6 | exbii 1582 |
. . 3
⊢ (∃y(x ∈ y ∧ y ∈ ℘1A) ↔ ∃y∃z ∈ A (y = {z} ∧ x ∈ y)) |
8 | | risset 2661 |
. . . 4
⊢ (x ∈ A ↔ ∃z ∈ A z = x) |
9 | | snex 4111 |
. . . . . . 7
⊢ {z} ∈
V |
10 | | eleq2 2414 |
. . . . . . 7
⊢ (y = {z} →
(x ∈
y ↔ x ∈ {z})) |
11 | 9, 10 | ceqsexv 2894 |
. . . . . 6
⊢ (∃y(y = {z} ∧ x ∈ y) ↔
x ∈
{z}) |
12 | | df-sn 3741 |
. . . . . . 7
⊢ {z} = {x ∣ x = z} |
13 | 12 | abeq2i 2460 |
. . . . . 6
⊢ (x ∈ {z} ↔ x =
z) |
14 | | equcom 1680 |
. . . . . 6
⊢ (x = z ↔
z = x) |
15 | 11, 13, 14 | 3bitri 262 |
. . . . 5
⊢ (∃y(y = {z} ∧ x ∈ y) ↔
z = x) |
16 | 15 | rexbii 2639 |
. . . 4
⊢ (∃z ∈ A ∃y(y = {z} ∧ x ∈ y) ↔
∃z ∈ A z = x) |
17 | | rexcom4 2878 |
. . . 4
⊢ (∃z ∈ A ∃y(y = {z} ∧ x ∈ y) ↔
∃y∃z ∈ A (y = {z} ∧ x ∈ y)) |
18 | 8, 16, 17 | 3bitr2ri 265 |
. . 3
⊢ (∃y∃z ∈ A (y = {z} ∧ x ∈ y) ↔
x ∈
A) |
19 | 1, 7, 18 | 3bitri 262 |
. 2
⊢ (x ∈ ∪℘1A ↔ x ∈ A) |
20 | 19 | eqriv 2350 |
1
⊢ ∪℘1A = A |