Theorem axrep6

Description: A condensed form of ax-rep . (Contributed by SN, 18-Sep-2023) (Proof shortened by Matthew House, 18-Sep-2025)

	Ref	Expression
Assertion	axrep6	$$⊢\forall w{\exists }^{*}z\phi \to \exists y\forall z\left(z\in y\leftrightarrow \exists w\in x\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		axrep4v	$$⊢\forall w\exists y\forall z\left(\phi \to z=y\right)\to \exists y\forall z\left(z\in y\leftrightarrow \exists w\left(w\in x\wedge \phi \right)\right)$$
2		dfmo	$$⊢{\exists }^{*}z\phi \leftrightarrow \exists y\forall z\left(\phi \to z=y\right)$$
3	2	albii	$$⊢\forall w{\exists }^{*}z\phi \leftrightarrow \forall w\exists y\forall z\left(\phi \to z=y\right)$$
4		df-rex	$$⊢\exists w\in x\phi \leftrightarrow \exists w\left(w\in x\wedge \phi \right)$$
5	4	bibi2i	$$⊢\left(z\in y\leftrightarrow \exists w\in x\phi \right)\leftrightarrow \left(z\in y\leftrightarrow \exists w\left(w\in x\wedge \phi \right)\right)$$
6	5	albii	$$⊢\forall z\left(z\in y\leftrightarrow \exists w\in x\phi \right)\leftrightarrow \forall z\left(z\in y\leftrightarrow \exists w\left(w\in x\wedge \phi \right)\right)$$
7	6	exbii	$$⊢\exists y\forall z\left(z\in y\leftrightarrow \exists w\in x\phi \right)\leftrightarrow \exists y\forall z\left(z\in y\leftrightarrow \exists w\left(w\in x\wedge \phi \right)\right)$$
8	1 3 7	3imtr4i	$$⊢\forall w{\exists }^{*}z\phi \to \exists y\forall z\left(z\in y\leftrightarrow \exists w\in x\phi \right)$$