Step | Hyp | Ref
| Expression |
1 | | bdsepnft.1 |
. . 3
⊢
BOUNDED 𝜑 |
2 | 1 | bdsep2 13661 |
. 2
⊢
∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑)) |
3 | | nfnf1 1531 |
. . . 4
⊢
Ⅎ𝑏Ⅎ𝑏𝜑 |
4 | 3 | nfal 1563 |
. . 3
⊢
Ⅎ𝑏∀𝑥Ⅎ𝑏𝜑 |
5 | | nfa1 1528 |
. . . 4
⊢
Ⅎ𝑥∀𝑥Ⅎ𝑏𝜑 |
6 | | nfvd 1516 |
. . . . 5
⊢
(∀𝑥Ⅎ𝑏𝜑 → Ⅎ𝑏 𝑥 ∈ 𝑦) |
7 | | nfv 1515 |
. . . . . . 7
⊢
Ⅎ𝑏 𝑥 ∈ 𝑎 |
8 | 7 | a1i 9 |
. . . . . 6
⊢
(∀𝑥Ⅎ𝑏𝜑 → Ⅎ𝑏 𝑥 ∈ 𝑎) |
9 | | sp 1498 |
. . . . . 6
⊢
(∀𝑥Ⅎ𝑏𝜑 → Ⅎ𝑏𝜑) |
10 | 8, 9 | nfand 1555 |
. . . . 5
⊢
(∀𝑥Ⅎ𝑏𝜑 → Ⅎ𝑏(𝑥 ∈ 𝑎 ∧ 𝜑)) |
11 | 6, 10 | nfbid 1575 |
. . . 4
⊢
(∀𝑥Ⅎ𝑏𝜑 → Ⅎ𝑏(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑))) |
12 | 5, 11 | nfald 1747 |
. . 3
⊢
(∀𝑥Ⅎ𝑏𝜑 → Ⅎ𝑏∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑))) |
13 | | nfv 1515 |
. . . . . 6
⊢
Ⅎ𝑥 𝑦 = 𝑏 |
14 | 5, 13 | nfan 1552 |
. . . . 5
⊢
Ⅎ𝑥(∀𝑥Ⅎ𝑏𝜑 ∧ 𝑦 = 𝑏) |
15 | | elequ2 2140 |
. . . . . . 7
⊢ (𝑦 = 𝑏 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑏)) |
16 | 15 | adantl 275 |
. . . . . 6
⊢
((∀𝑥Ⅎ𝑏𝜑 ∧ 𝑦 = 𝑏) → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑏)) |
17 | 16 | bibi1d 232 |
. . . . 5
⊢
((∀𝑥Ⅎ𝑏𝜑 ∧ 𝑦 = 𝑏) → ((𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑)) ↔ (𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑)))) |
18 | 14, 17 | albid 1602 |
. . . 4
⊢
((∀𝑥Ⅎ𝑏𝜑 ∧ 𝑦 = 𝑏) → (∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑)) ↔ ∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑)))) |
19 | 18 | ex 114 |
. . 3
⊢
(∀𝑥Ⅎ𝑏𝜑 → (𝑦 = 𝑏 → (∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑)) ↔ ∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑))))) |
20 | 4, 12, 19 | cbvexd 1914 |
. 2
⊢
(∀𝑥Ⅎ𝑏𝜑 → (∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑)) ↔ ∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑)))) |
21 | 2, 20 | mpbii 147 |
1
⊢
(∀𝑥Ⅎ𝑏𝜑 → ∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑))) |