Step | Hyp | Ref
| Expression |
1 | | pw1ss1c 4158 |
. . 3
⊢ ℘1B ⊆
1c |
2 | | sseq1 3292 |
. . 3
⊢ (A = ℘1B → (A
⊆ 1c ↔ ℘1B ⊆
1c)) |
3 | 1, 2 | mpbiri 224 |
. 2
⊢ (A = ℘1B → A ⊆ 1c) |
4 | | ssofeq 4077 |
. . . 4
⊢ ((A ⊆
1c ∧ ℘1B ⊆
1c) → (A = ℘1B ↔ ∀y ∈ 1c (y ∈ A ↔ y ∈ ℘1B))) |
5 | 1, 4 | mpan2 652 |
. . 3
⊢ (A ⊆
1c → (A = ℘1B ↔ ∀y ∈ 1c (y ∈ A ↔ y ∈ ℘1B))) |
6 | | df-ral 2619 |
. . . . 5
⊢ (∀y ∈ 1c (y ∈ A ↔ y ∈ ℘1B) ↔ ∀y(y ∈
1c → (y ∈ A ↔
y ∈ ℘1B))) |
7 | | el1c 4139 |
. . . . . . . . 9
⊢ (y ∈
1c ↔ ∃x y = {x}) |
8 | 7 | imbi1i 315 |
. . . . . . . 8
⊢ ((y ∈
1c → (y ∈ A ↔
y ∈ ℘1B)) ↔ (∃x y = {x} →
(y ∈
A ↔ y ∈ ℘1B))) |
9 | | 19.23v 1891 |
. . . . . . . 8
⊢ (∀x(y = {x} →
(y ∈
A ↔ y ∈ ℘1B)) ↔ (∃x y = {x} →
(y ∈
A ↔ y ∈ ℘1B))) |
10 | 8, 9 | bitr4i 243 |
. . . . . . 7
⊢ ((y ∈
1c → (y ∈ A ↔
y ∈ ℘1B)) ↔ ∀x(y = {x} →
(y ∈
A ↔ y ∈ ℘1B))) |
11 | 10 | albii 1566 |
. . . . . 6
⊢ (∀y(y ∈
1c → (y ∈ A ↔
y ∈ ℘1B)) ↔ ∀y∀x(y = {x} →
(y ∈
A ↔ y ∈ ℘1B))) |
12 | | alcom 1737 |
. . . . . 6
⊢ (∀x∀y(y = {x} →
(y ∈
A ↔ y ∈ ℘1B)) ↔ ∀y∀x(y = {x} →
(y ∈
A ↔ y ∈ ℘1B))) |
13 | 11, 12 | bitr4i 243 |
. . . . 5
⊢ (∀y(y ∈
1c → (y ∈ A ↔
y ∈ ℘1B)) ↔ ∀x∀y(y = {x} →
(y ∈
A ↔ y ∈ ℘1B))) |
14 | 6, 13 | bitri 240 |
. . . 4
⊢ (∀y ∈ 1c (y ∈ A ↔ y ∈ ℘1B) ↔ ∀x∀y(y = {x} →
(y ∈
A ↔ y ∈ ℘1B))) |
15 | | snex 4111 |
. . . . . . 7
⊢ {x} ∈
V |
16 | | eleq1 2413 |
. . . . . . . 8
⊢ (y = {x} →
(y ∈
A ↔ {x} ∈ A)) |
17 | | eleq1 2413 |
. . . . . . . 8
⊢ (y = {x} →
(y ∈
℘1B ↔ {x}
∈ ℘1B)) |
18 | 16, 17 | bibi12d 312 |
. . . . . . 7
⊢ (y = {x} →
((y ∈
A ↔ y ∈ ℘1B) ↔ ({x}
∈ A
↔ {x} ∈ ℘1B))) |
19 | 15, 18 | ceqsalv 2885 |
. . . . . 6
⊢ (∀y(y = {x} →
(y ∈
A ↔ y ∈ ℘1B)) ↔ ({x}
∈ A
↔ {x} ∈ ℘1B)) |
20 | | snelpw1 4146 |
. . . . . . 7
⊢ ({x} ∈ ℘1B ↔ x ∈ B) |
21 | 20 | bibi2i 304 |
. . . . . 6
⊢ (({x} ∈ A ↔ {x}
∈ ℘1B) ↔ ({x}
∈ A
↔ x ∈ B)) |
22 | 19, 21 | bitri 240 |
. . . . 5
⊢ (∀y(y = {x} →
(y ∈
A ↔ y ∈ ℘1B)) ↔ ({x}
∈ A
↔ x ∈ B)) |
23 | 22 | albii 1566 |
. . . 4
⊢ (∀x∀y(y = {x} →
(y ∈
A ↔ y ∈ ℘1B)) ↔ ∀x({x} ∈ A ↔ x ∈ B)) |
24 | 14, 23 | bitri 240 |
. . 3
⊢ (∀y ∈ 1c (y ∈ A ↔ y ∈ ℘1B) ↔ ∀x({x} ∈ A ↔ x ∈ B)) |
25 | 5, 24 | syl6bb 252 |
. 2
⊢ (A ⊆
1c → (A = ℘1B ↔ ∀x({x} ∈ A ↔ x ∈ B))) |
26 | 3, 25 | biadan2 623 |
1
⊢ (A = ℘1B ↔ (A
⊆ 1c ∧ ∀x({x} ∈ A ↔
x ∈
B))) |