Step | Hyp | Ref
| Expression |
1 | | nfv 1418 |
. . . . . . . 8
⊢
Ⅎx y ∈ z |
2 | | bm1.1.1 |
. . . . . . . 8
⊢
Ⅎxφ |
3 | 1, 2 | nfbi 1478 |
. . . . . . 7
⊢
Ⅎx(y ∈ z ↔ φ) |
4 | 3 | nfal 1465 |
. . . . . 6
⊢
Ⅎx∀y(y ∈ z ↔ φ) |
5 | | elequ2 1598 |
. . . . . . . 8
⊢ (x = z →
(y ∈
x ↔ y ∈ z)) |
6 | 5 | bibi1d 222 |
. . . . . . 7
⊢ (x = z →
((y ∈
x ↔ φ) ↔ (y ∈ z ↔ φ))) |
7 | 6 | albidv 1702 |
. . . . . 6
⊢ (x = z →
(∀y(y ∈ x ↔
φ) ↔ ∀y(y ∈ z ↔ φ))) |
8 | 4, 7 | sbie 1671 |
. . . . 5
⊢
([z / x]∀y(y ∈ x ↔
φ) ↔ ∀y(y ∈ z ↔ φ)) |
9 | | 19.26 1367 |
. . . . . 6
⊢ (∀y((y ∈ x ↔ φ)
∧ (y ∈ z ↔
φ)) ↔ (∀y(y ∈ x ↔ φ)
∧ ∀y(y ∈ z ↔ φ))) |
10 | | biantr 858 |
. . . . . . . 8
⊢
(((y ∈ x ↔
φ) ∧
(y ∈
z ↔ φ)) → (y ∈ x ↔ y ∈ z)) |
11 | 10 | alimi 1341 |
. . . . . . 7
⊢ (∀y((y ∈ x ↔ φ)
∧ (y ∈ z ↔
φ)) → ∀y(y ∈ x ↔ y ∈ z)) |
12 | | ax-ext 2019 |
. . . . . . 7
⊢ (∀y(y ∈ x ↔ y ∈ z) →
x = z) |
13 | 11, 12 | syl 14 |
. . . . . 6
⊢ (∀y((y ∈ x ↔ φ)
∧ (y ∈ z ↔
φ)) → x = z) |
14 | 9, 13 | sylbir 125 |
. . . . 5
⊢ ((∀y(y ∈ x ↔ φ)
∧ ∀y(y ∈ z ↔ φ))
→ x = z) |
15 | 8, 14 | sylan2b 271 |
. . . 4
⊢ ((∀y(y ∈ x ↔ φ)
∧ [z /
x]∀y(y ∈ x ↔ φ))
→ x = z) |
16 | 15 | gen2 1336 |
. . 3
⊢ ∀x∀z((∀y(y ∈ x ↔ φ)
∧ [z /
x]∀y(y ∈ x ↔ φ))
→ x = z) |
17 | 16 | jctr 298 |
. 2
⊢ (∃x∀y(y ∈ x ↔ φ)
→ (∃x∀y(y ∈ x ↔
φ) ∧
∀x∀z((∀y(y ∈ x ↔ φ)
∧ [z /
x]∀y(y ∈ x ↔ φ))
→ x = z))) |
18 | | nfv 1418 |
. . 3
⊢
Ⅎz∀y(y ∈ x ↔ φ) |
19 | 18 | eu2 1941 |
. 2
⊢ (∃!x∀y(y ∈ x ↔ φ)
↔ (∃x∀y(y ∈ x ↔
φ) ∧
∀x∀z((∀y(y ∈ x ↔ φ)
∧ [z /
x]∀y(y ∈ x ↔ φ))
→ x = z))) |
20 | 17, 19 | sylibr 137 |
1
⊢ (∃x∀y(y ∈ x ↔ φ)
→ ∃!x∀y(y ∈ x ↔
φ)) |