Step | Hyp | Ref
| Expression |
1 | | elpw1 4144 |
. 2
⊢ (A ∈ ℘1℘1℘1℘1℘1℘1℘1℘1℘1℘11c ↔ ∃y ∈ ℘1
℘1℘1℘1℘1℘1℘1℘1℘11cA = {y}) |
2 | | df-rex 2620 |
. . . 4
⊢ (∃y ∈ ℘1
℘1℘1℘1℘1℘1℘1℘1℘11cA = {y} ↔
∃y(y ∈ ℘1℘1℘1℘1℘1℘1℘1℘1℘11c ∧ A = {y})) |
3 | | elpw191c 4155 |
. . . . . . 7
⊢ (y ∈ ℘1℘1℘1℘1℘1℘1℘1℘1℘11c ↔ ∃x y = {{{{{{{{{{x}}}}}}}}}}) |
4 | 3 | anbi1i 676 |
. . . . . 6
⊢ ((y ∈ ℘1℘1℘1℘1℘1℘1℘1℘1℘11c ∧ A = {y}) ↔ (∃x y = {{{{{{{{{{x}}}}}}}}}} ∧
A = {y})) |
5 | | 19.41v 1901 |
. . . . . 6
⊢ (∃x(y = {{{{{{{{{{x}}}}}}}}}} ∧
A = {y}) ↔ (∃x y = {{{{{{{{{{x}}}}}}}}}} ∧
A = {y})) |
6 | 4, 5 | bitr4i 243 |
. . . . 5
⊢ ((y ∈ ℘1℘1℘1℘1℘1℘1℘1℘1℘11c ∧ A = {y}) ↔ ∃x(y = {{{{{{{{{{x}}}}}}}}}} ∧
A = {y})) |
7 | 6 | exbii 1582 |
. . . 4
⊢ (∃y(y ∈ ℘1℘1℘1℘1℘1℘1℘1℘1℘11c ∧ A = {y}) ↔ ∃y∃x(y = {{{{{{{{{{x}}}}}}}}}} ∧
A = {y})) |
8 | 2, 7 | bitri 240 |
. . 3
⊢ (∃y ∈ ℘1
℘1℘1℘1℘1℘1℘1℘1℘11cA = {y} ↔
∃y∃x(y = {{{{{{{{{{x}}}}}}}}}} ∧
A = {y})) |
9 | | excom 1741 |
. . . 4
⊢ (∃y∃x(y = {{{{{{{{{{x}}}}}}}}}} ∧
A = {y}) ↔ ∃x∃y(y = {{{{{{{{{{x}}}}}}}}}} ∧
A = {y})) |
10 | | snex 4111 |
. . . . . 6
⊢ {{{{{{{{{{x}}}}}}}}}} ∈
V |
11 | | sneq 3744 |
. . . . . . 7
⊢ (y = {{{{{{{{{{x}}}}}}}}}} → {y} = {{{{{{{{{{{x}}}}}}}}}}}) |
12 | 11 | eqeq2d 2364 |
. . . . . 6
⊢ (y = {{{{{{{{{{x}}}}}}}}}} → (A = {y} ↔
A = {{{{{{{{{{{x}}}}}}}}}}})) |
13 | 10, 12 | ceqsexv 2894 |
. . . . 5
⊢ (∃y(y = {{{{{{{{{{x}}}}}}}}}} ∧
A = {y}) ↔ A =
{{{{{{{{{{{x}}}}}}}}}}}) |
14 | 13 | exbii 1582 |
. . . 4
⊢ (∃x∃y(y = {{{{{{{{{{x}}}}}}}}}} ∧
A = {y}) ↔ ∃x A = {{{{{{{{{{{x}}}}}}}}}}}) |
15 | 9, 14 | bitri 240 |
. . 3
⊢ (∃y∃x(y = {{{{{{{{{{x}}}}}}}}}} ∧
A = {y}) ↔ ∃x A = {{{{{{{{{{{x}}}}}}}}}}}) |
16 | 8, 15 | bitri 240 |
. 2
⊢ (∃y ∈ ℘1
℘1℘1℘1℘1℘1℘1℘1℘11cA = {y} ↔
∃x
A = {{{{{{{{{{{x}}}}}}}}}}}) |
17 | 1, 16 | bitri 240 |
1
⊢ (A ∈ ℘1℘1℘1℘1℘1℘1℘1℘1℘1℘11c ↔ ∃x A = {{{{{{{{{{{x}}}}}}}}}}}) |