Theorem sepex

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	⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 ∈ 𝑦 ) → ∃ 𝑧 ∀ 𝑥 ( 𝑥 ∈ 𝑧 ↔ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		sepexlem	⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 ∈ 𝑦 ) → ∃ 𝑤 ∀ 𝑥 ( 𝑥 ∈ 𝑤 ↔ 𝜑 ) )
2		biimpr	⊢ ( ( 𝑥 ∈ 𝑤 ↔ 𝜑 ) → ( 𝜑 → 𝑥 ∈ 𝑤 ) )
3	2	alimi	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑤 ↔ 𝜑 ) → ∀ 𝑥 ( 𝜑 → 𝑥 ∈ 𝑤 ) )
4	3	eximi	⊢ ( ∃ 𝑤 ∀ 𝑥 ( 𝑥 ∈ 𝑤 ↔ 𝜑 ) → ∃ 𝑤 ∀ 𝑥 ( 𝜑 → 𝑥 ∈ 𝑤 ) )
5		sepexlem	⊢ ( ∃ 𝑤 ∀ 𝑥 ( 𝜑 → 𝑥 ∈ 𝑤 ) → ∃ 𝑧 ∀ 𝑥 ( 𝑥 ∈ 𝑧 ↔ 𝜑 ) )
6	1 4 5	3syl	⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 ∈ 𝑦 ) → ∃ 𝑧 ∀ 𝑥 ( 𝑥 ∈ 𝑧 ↔ 𝜑 ) )