Step | Hyp | Ref
| Expression |
1 | | bdsepnft.1 |
. . 3
⊢
BOUNDED φ |
2 | 1 | bdsep2 9341 |
. 2
⊢ ∃y∀x(x ∈ y ↔ (x
∈ 𝑎 ∧ φ)) |
3 | | nfnf1 1433 |
. . . 4
⊢
Ⅎ𝑏Ⅎ𝑏φ |
4 | 3 | nfal 1465 |
. . 3
⊢
Ⅎ𝑏∀xℲ𝑏φ |
5 | | nfa1 1431 |
. . . 4
⊢
Ⅎx∀xℲ𝑏φ |
6 | | nfvd 1419 |
. . . . 5
⊢ (∀xℲ𝑏φ
→ Ⅎ𝑏 x ∈ y) |
7 | | nfv 1418 |
. . . . . . 7
⊢
Ⅎ𝑏 x ∈ 𝑎 |
8 | 7 | a1i 9 |
. . . . . 6
⊢ (∀xℲ𝑏φ
→ Ⅎ𝑏 x ∈ 𝑎) |
9 | | sp 1398 |
. . . . . 6
⊢ (∀xℲ𝑏φ
→ Ⅎ𝑏φ) |
10 | 8, 9 | nfand 1457 |
. . . . 5
⊢ (∀xℲ𝑏φ
→ Ⅎ𝑏(x ∈ 𝑎 ∧
φ)) |
11 | 6, 10 | nfbid 1477 |
. . . 4
⊢ (∀xℲ𝑏φ
→ Ⅎ𝑏(x ∈ y ↔ (x
∈ 𝑎 ∧ φ))) |
12 | 5, 11 | nfald 1640 |
. . 3
⊢ (∀xℲ𝑏φ
→ Ⅎ𝑏∀x(x ∈ y ↔ (x
∈ 𝑎 ∧ φ))) |
13 | | nfv 1418 |
. . . . . 6
⊢
Ⅎx y = 𝑏 |
14 | 5, 13 | nfan 1454 |
. . . . 5
⊢
Ⅎx(∀xℲ𝑏φ
∧ y =
𝑏) |
15 | | elequ2 1598 |
. . . . . . 7
⊢ (y = 𝑏 → (x ∈ y ↔ x ∈ 𝑏)) |
16 | 15 | adantl 262 |
. . . . . 6
⊢ ((∀xℲ𝑏φ
∧ y =
𝑏) → (x ∈ y ↔ x ∈ 𝑏)) |
17 | 16 | bibi1d 222 |
. . . . 5
⊢ ((∀xℲ𝑏φ
∧ y =
𝑏) → ((x ∈ y ↔ (x
∈ 𝑎 ∧ φ)) ↔ (x ∈ 𝑏 ↔ (x ∈ 𝑎 ∧
φ)))) |
18 | 14, 17 | albid 1503 |
. . . 4
⊢ ((∀xℲ𝑏φ
∧ y =
𝑏) → (∀x(x ∈ y ↔ (x
∈ 𝑎 ∧ φ)) ↔ ∀x(x ∈ 𝑏 ↔ (x ∈ 𝑎 ∧
φ)))) |
19 | 18 | ex 108 |
. . 3
⊢ (∀xℲ𝑏φ
→ (y = 𝑏 → (∀x(x ∈ y ↔ (x
∈ 𝑎 ∧ φ)) ↔ ∀x(x ∈ 𝑏 ↔ (x ∈ 𝑎 ∧
φ))))) |
20 | 4, 12, 19 | cbvexd 1799 |
. 2
⊢ (∀xℲ𝑏φ
→ (∃y∀x(x ∈ y ↔
(x ∈
𝑎 ∧ φ)) ↔
∃𝑏∀x(x ∈ 𝑏 ↔ (x ∈ 𝑎 ∧
φ)))) |
21 | 2, 20 | mpbii 136 |
1
⊢ (∀xℲ𝑏φ
→ ∃𝑏∀x(x ∈ 𝑏 ↔ (x ∈ 𝑎 ∧
φ))) |