Step | Hyp | Ref
| Expression |
1 | | nfv 1508 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑦 ∈ 𝑧 |
2 | | bm1.1.1 |
. . . . . . . 8
⊢
Ⅎ𝑥𝜑 |
3 | 1, 2 | nfbi 1569 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑦 ∈ 𝑧 ↔ 𝜑) |
4 | 3 | nfal 1556 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑦(𝑦 ∈ 𝑧 ↔ 𝜑) |
5 | | elequ2 2133 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧)) |
6 | 5 | bibi1d 232 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ((𝑦 ∈ 𝑥 ↔ 𝜑) ↔ (𝑦 ∈ 𝑧 ↔ 𝜑))) |
7 | 6 | albidv 1804 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝑧 ↔ 𝜑))) |
8 | 4, 7 | sbie 1771 |
. . . . 5
⊢ ([𝑧 / 𝑥]∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝑧 ↔ 𝜑)) |
9 | | 19.26 1461 |
. . . . . 6
⊢
(∀𝑦((𝑦 ∈ 𝑥 ↔ 𝜑) ∧ (𝑦 ∈ 𝑧 ↔ 𝜑)) ↔ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑) ∧ ∀𝑦(𝑦 ∈ 𝑧 ↔ 𝜑))) |
10 | | biantr 937 |
. . . . . . . 8
⊢ (((𝑦 ∈ 𝑥 ↔ 𝜑) ∧ (𝑦 ∈ 𝑧 ↔ 𝜑)) → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧)) |
11 | 10 | alimi 1435 |
. . . . . . 7
⊢
(∀𝑦((𝑦 ∈ 𝑥 ↔ 𝜑) ∧ (𝑦 ∈ 𝑧 ↔ 𝜑)) → ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧)) |
12 | | ax-ext 2139 |
. . . . . . 7
⊢
(∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧) → 𝑥 = 𝑧) |
13 | 11, 12 | syl 14 |
. . . . . 6
⊢
(∀𝑦((𝑦 ∈ 𝑥 ↔ 𝜑) ∧ (𝑦 ∈ 𝑧 ↔ 𝜑)) → 𝑥 = 𝑧) |
14 | 9, 13 | sylbir 134 |
. . . . 5
⊢
((∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑) ∧ ∀𝑦(𝑦 ∈ 𝑧 ↔ 𝜑)) → 𝑥 = 𝑧) |
15 | 8, 14 | sylan2b 285 |
. . . 4
⊢
((∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑) ∧ [𝑧 / 𝑥]∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑)) → 𝑥 = 𝑧) |
16 | 15 | gen2 1430 |
. . 3
⊢
∀𝑥∀𝑧((∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑) ∧ [𝑧 / 𝑥]∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑)) → 𝑥 = 𝑧) |
17 | 16 | jctr 313 |
. 2
⊢
(∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑) → (∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑) ∧ ∀𝑥∀𝑧((∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑) ∧ [𝑧 / 𝑥]∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑)) → 𝑥 = 𝑧))) |
18 | | nfv 1508 |
. . 3
⊢
Ⅎ𝑧∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑) |
19 | 18 | eu2 2050 |
. 2
⊢
(∃!𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑) ↔ (∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑) ∧ ∀𝑥∀𝑧((∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑) ∧ [𝑧 / 𝑥]∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑)) → 𝑥 = 𝑧))) |
20 | 17, 19 | sylibr 133 |
1
⊢
(∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑) → ∃!𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑)) |