Theorem sepexlem

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

	Ref	Expression
Assertion	sepexlem	$$⊢\exists y\forall x\left(\phi \to x\in y\right)\to \exists z\forall x\left(x\in z\leftrightarrow \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ax-sep	$$⊢\exists z\forall x\left(x\in z\leftrightarrow \left(x\in y\wedge \phi \right)\right)$$
2		bimsc1	$$⊢\left(\left(\phi \to x\in y\right)\wedge \left(x\in z\leftrightarrow \left(x\in y\wedge \phi \right)\right)\right)\to \left(x\in z\leftrightarrow \phi \right)$$
3	2	ex	$$⊢\left(\phi \to x\in y\right)\to \left(\left(x\in z\leftrightarrow \left(x\in y\wedge \phi \right)\right)\to \left(x\in z\leftrightarrow \phi \right)\right)$$
4	3	al2imi	$$⊢\forall x\left(\phi \to x\in y\right)\to \left(\forall x\left(x\in z\leftrightarrow \left(x\in y\wedge \phi \right)\right)\to \forall x\left(x\in z\leftrightarrow \phi \right)\right)$$
5	4	eximdv	$$⊢\forall x\left(\phi \to x\in y\right)\to \left(\exists z\forall x\left(x\in z\leftrightarrow \left(x\in y\wedge \phi \right)\right)\to \exists z\forall x\left(x\in z\leftrightarrow \phi \right)\right)$$
6	1 5	mpi	$$⊢\forall x\left(\phi \to x\in y\right)\to \exists z\forall x\left(x\in z\leftrightarrow \phi \right)$$
7	6	exlimiv	$$⊢\exists y\forall x\left(\phi \to x\in y\right)\to \exists z\forall x\left(x\in z\leftrightarrow \phi \right)$$