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