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 (φ \to x \in y) \to \exists z \forall x (x \in z \leftrightarrow φ)$

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

Metamath Proof Explorer