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

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