This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sepexi

Description: Convert implication to equivalence within an existence statement using the Separation Scheme (Aussonderung) ax-sep . Inference associated with sepex . (Contributed by NM, 21-Jun-1993) Generalize conclusion, extract closed form, and avoid ax-9 . (Revised by Matthew House, 19-Sep-2025)

		Ref	Expression
	Hypothesis	sepexi.1	⊢ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 ∈ 𝑦 )
	Assertion	sepexi	⊢ ∃ 𝑧 ∀ 𝑥 ( 𝑥 ∈ 𝑧 ↔ 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sepexi.1	⊢ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 ∈ 𝑦 )
2		sepex	⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 ∈ 𝑦 ) → ∃ 𝑧 ∀ 𝑥 ( 𝑥 ∈ 𝑧 ↔ 𝜑 ) )
3	1 2	ax-mp	⊢ ∃ 𝑧 ∀ 𝑥 ( 𝑥 ∈ 𝑧 ↔ 𝜑 )