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 𝑧𝑥 ( 𝑥𝑧𝜑 )