Step | Hyp | Ref
| Expression |
1 | | elequ2 2125 |
. . . . 5
⊢ (𝑥 = 𝑡 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑡)) |
2 | 1 | imbi2d 341 |
. . . 4
⊢ (𝑥 = 𝑡 → ((𝜑 → 𝑧 ∈ 𝑥) ↔ (𝜑 → 𝑧 ∈ 𝑡))) |
3 | 2 | albidv 1927 |
. . 3
⊢ (𝑥 = 𝑡 → (∀𝑧(𝜑 → 𝑧 ∈ 𝑥) ↔ ∀𝑧(𝜑 → 𝑧 ∈ 𝑡))) |
4 | 3 | cbvexvw 2044 |
. 2
⊢
(∃𝑥∀𝑧(𝜑 → 𝑧 ∈ 𝑥) ↔ ∃𝑡∀𝑧(𝜑 → 𝑧 ∈ 𝑡)) |
5 | | ax-sep 5227 |
. . . . 5
⊢
∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑡 ∧ 𝜑)) |
6 | | 19.42v 1961 |
. . . . . 6
⊢
(∃𝑦(∀𝑧(𝜑 → 𝑧 ∈ 𝑡) ∧ ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑡 ∧ 𝜑))) ↔ (∀𝑧(𝜑 → 𝑧 ∈ 𝑡) ∧ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑡 ∧ 𝜑)))) |
7 | | bimsc1 841 |
. . . . . . . 8
⊢ (((𝜑 → 𝑧 ∈ 𝑡) ∧ (𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑡 ∧ 𝜑))) → (𝑧 ∈ 𝑦 ↔ 𝜑)) |
8 | 7 | alanimi 1823 |
. . . . . . 7
⊢
((∀𝑧(𝜑 → 𝑧 ∈ 𝑡) ∧ ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑡 ∧ 𝜑))) → ∀𝑧(𝑧 ∈ 𝑦 ↔ 𝜑)) |
9 | 8 | eximi 1841 |
. . . . . 6
⊢
(∃𝑦(∀𝑧(𝜑 → 𝑧 ∈ 𝑡) ∧ ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑡 ∧ 𝜑))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝜑)) |
10 | 6, 9 | sylbir 234 |
. . . . 5
⊢
((∀𝑧(𝜑 → 𝑧 ∈ 𝑡) ∧ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑡 ∧ 𝜑))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝜑)) |
11 | 5, 10 | mpan2 688 |
. . . 4
⊢
(∀𝑧(𝜑 → 𝑧 ∈ 𝑡) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝜑)) |
12 | 11 | exlimiv 1937 |
. . 3
⊢
(∃𝑡∀𝑧(𝜑 → 𝑧 ∈ 𝑡) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝜑)) |
13 | | elequ2 2125 |
. . . . . . 7
⊢ (𝑦 = 𝑡 → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑡)) |
14 | 13 | bibi1d 344 |
. . . . . 6
⊢ (𝑦 = 𝑡 → ((𝑧 ∈ 𝑦 ↔ 𝜑) ↔ (𝑧 ∈ 𝑡 ↔ 𝜑))) |
15 | 14 | albidv 1927 |
. . . . 5
⊢ (𝑦 = 𝑡 → (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝜑) ↔ ∀𝑧(𝑧 ∈ 𝑡 ↔ 𝜑))) |
16 | 15 | cbvexvw 2044 |
. . . 4
⊢
(∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝜑) ↔ ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ 𝜑)) |
17 | | biimpr 219 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑡 ↔ 𝜑) → (𝜑 → 𝑧 ∈ 𝑡)) |
18 | 17 | alimi 1818 |
. . . . 5
⊢
(∀𝑧(𝑧 ∈ 𝑡 ↔ 𝜑) → ∀𝑧(𝜑 → 𝑧 ∈ 𝑡)) |
19 | 18 | eximi 1841 |
. . . 4
⊢
(∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ 𝜑) → ∃𝑡∀𝑧(𝜑 → 𝑧 ∈ 𝑡)) |
20 | 16, 19 | sylbi 216 |
. . 3
⊢
(∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝜑) → ∃𝑡∀𝑧(𝜑 → 𝑧 ∈ 𝑡)) |
21 | 12, 20 | impbii 208 |
. 2
⊢
(∃𝑡∀𝑧(𝜑 → 𝑧 ∈ 𝑡) ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝜑)) |
22 | 4, 21 | bitri 274 |
1
⊢
(∃𝑥∀𝑧(𝜑 → 𝑧 ∈ 𝑥) ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝜑)) |