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