Metamath Proof Explorer


Theorem sepexlem

Description: Lemma for sepex . Use sepex instead. (Contributed by Matthew House, 19-Sep-2025) (New usage is discouraged.)

Ref Expression
Assertion sepexlem ( ∃ 𝑦𝑥 ( 𝜑𝑥𝑦 ) → ∃ 𝑧𝑥 ( 𝑥𝑧𝜑 ) )

Proof

Step Hyp Ref Expression
1 ax-sep 𝑧𝑥 ( 𝑥𝑧 ↔ ( 𝑥𝑦𝜑 ) )
2 bimsc1 ( ( ( 𝜑𝑥𝑦 ) ∧ ( 𝑥𝑧 ↔ ( 𝑥𝑦𝜑 ) ) ) → ( 𝑥𝑧𝜑 ) )
3 2 ex ( ( 𝜑𝑥𝑦 ) → ( ( 𝑥𝑧 ↔ ( 𝑥𝑦𝜑 ) ) → ( 𝑥𝑧𝜑 ) ) )
4 3 al2imi ( ∀ 𝑥 ( 𝜑𝑥𝑦 ) → ( ∀ 𝑥 ( 𝑥𝑧 ↔ ( 𝑥𝑦𝜑 ) ) → ∀ 𝑥 ( 𝑥𝑧𝜑 ) ) )
5 4 eximdv ( ∀ 𝑥 ( 𝜑𝑥𝑦 ) → ( ∃ 𝑧𝑥 ( 𝑥𝑧 ↔ ( 𝑥𝑦𝜑 ) ) → ∃ 𝑧𝑥 ( 𝑥𝑧𝜑 ) ) )
6 1 5 mpi ( ∀ 𝑥 ( 𝜑𝑥𝑦 ) → ∃ 𝑧𝑥 ( 𝑥𝑧𝜑 ) )
7 6 exlimiv ( ∃ 𝑦𝑥 ( 𝜑𝑥𝑦 ) → ∃ 𝑧𝑥 ( 𝑥𝑧𝜑 ) )