Description: Convert implication to equivalence within an existence statement using the Separation Scheme (Aussonderung) ax-sep . Similar to Theorem 1.3(ii) of BellMachover p. 463. (Contributed by Matthew House, 19-Sep-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sepex | ⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 ∈ 𝑦 ) → ∃ 𝑧 ∀ 𝑥 ( 𝑥 ∈ 𝑧 ↔ 𝜑 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sepexlem | ⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 ∈ 𝑦 ) → ∃ 𝑤 ∀ 𝑥 ( 𝑥 ∈ 𝑤 ↔ 𝜑 ) ) | |
| 2 | biimpr | ⊢ ( ( 𝑥 ∈ 𝑤 ↔ 𝜑 ) → ( 𝜑 → 𝑥 ∈ 𝑤 ) ) | |
| 3 | 2 | alimi | ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑤 ↔ 𝜑 ) → ∀ 𝑥 ( 𝜑 → 𝑥 ∈ 𝑤 ) ) |
| 4 | 3 | eximi | ⊢ ( ∃ 𝑤 ∀ 𝑥 ( 𝑥 ∈ 𝑤 ↔ 𝜑 ) → ∃ 𝑤 ∀ 𝑥 ( 𝜑 → 𝑥 ∈ 𝑤 ) ) |
| 5 | sepexlem | ⊢ ( ∃ 𝑤 ∀ 𝑥 ( 𝜑 → 𝑥 ∈ 𝑤 ) → ∃ 𝑧 ∀ 𝑥 ( 𝑥 ∈ 𝑧 ↔ 𝜑 ) ) | |
| 6 | 1 4 5 | 3syl | ⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 ∈ 𝑦 ) → ∃ 𝑧 ∀ 𝑥 ( 𝑥 ∈ 𝑧 ↔ 𝜑 ) ) |