Proof of Theorem axrep4v
Step | Hyp | Ref
| Expression |
1 | | ax-rep 5284 |
. 2
⊢
(∀𝑥∃𝑧∀𝑦(∀𝑧𝜑 → 𝑦 = 𝑧) → ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑧𝜑))) |
2 | | 19.3v 1978 |
. . . . . 6
⊢
(∀𝑧𝜑 ↔ 𝜑) |
3 | 2 | imbi1i 349 |
. . . . 5
⊢
((∀𝑧𝜑 → 𝑦 = 𝑧) ↔ (𝜑 → 𝑦 = 𝑧)) |
4 | 3 | albii 1815 |
. . . 4
⊢
(∀𝑦(∀𝑧𝜑 → 𝑦 = 𝑧) ↔ ∀𝑦(𝜑 → 𝑦 = 𝑧)) |
5 | 4 | exbii 1844 |
. . 3
⊢
(∃𝑧∀𝑦(∀𝑧𝜑 → 𝑦 = 𝑧) ↔ ∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧)) |
6 | 5 | albii 1815 |
. 2
⊢
(∀𝑥∃𝑧∀𝑦(∀𝑧𝜑 → 𝑦 = 𝑧) ↔ ∀𝑥∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧)) |
7 | 2 | anbi2i 623 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑤 ∧ ∀𝑧𝜑) ↔ (𝑥 ∈ 𝑤 ∧ 𝜑)) |
8 | 7 | exbii 1844 |
. . . . 5
⊢
(∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑧𝜑) ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)) |
9 | 8 | bibi2i 337 |
. . . 4
⊢ ((𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑧𝜑)) ↔ (𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑))) |
10 | 9 | albii 1815 |
. . 3
⊢
(∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑧𝜑)) ↔ ∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑))) |
11 | 10 | exbii 1844 |
. 2
⊢
(∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑧𝜑)) ↔ ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑))) |
12 | 1, 6, 11 | 3imtr3i 291 |
1
⊢
(∀𝑥∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧) → ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑))) |