Theorem zfrep6

Description: A version of the Axiom of Replacement. Normally ph would have free variables x and y . Axiom 6 of Kunen p. 12. The Separation Scheme ax-sep cannot be derived from this version and must be stated as a separate axiom in an axiom system (such as Kunen's) that uses this version in place of our ax-rep . (Contributed by NM, 10-Oct-2003) Shorten proof and reduce axiom dependencies. (Revised by BJ, 5-Apr-2026)

	Ref	Expression
Assertion	zfrep6	$$⊢\forall x\in z\exists !y\phi \to \exists w\forall x\in z\exists y\in w\phi$$

Proof

Step	Hyp	Ref	Expression
1		euex	$$⊢\exists !y\phi \to \exists y\phi$$
2	1	ralimi	$$⊢\forall x\in z\exists !y\phi \to \forall x\in z\exists y\phi$$
3		df-ral	$$⊢\forall x\in z\exists !y\phi \leftrightarrow \forall x\left(x\in z\to \exists !y\phi \right)$$
4		eumo	$$⊢\exists !y\phi \to {\exists }^{*}y\phi$$
5	4	imim2i	$$⊢\left(x\in z\to \exists !y\phi \right)\to \left(x\in z\to {\exists }^{*}y\phi \right)$$
6		moanimv	$$⊢{\exists }^{*}y\left(x\in z\wedge \phi \right)\leftrightarrow \left(x\in z\to {\exists }^{*}y\phi \right)$$
7	5 6	sylibr	$$⊢\left(x\in z\to \exists !y\phi \right)\to {\exists }^{*}y\left(x\in z\wedge \phi \right)$$
8	7	alimi	$$⊢\forall x\left(x\in z\to \exists !y\phi \right)\to \forall x{\exists }^{*}y\left(x\in z\wedge \phi \right)$$
9	3 8	sylbi	$$⊢\forall x\in z\exists !y\phi \to \forall x{\exists }^{*}y\left(x\in z\wedge \phi \right)$$
10		axrep6	$$⊢\forall x{\exists }^{*}y\left(x\in z\wedge \phi \right)\to \exists w\forall y\left(y\in w\leftrightarrow \exists x\in z\left(x\in z\wedge \phi \right)\right)$$
11		rexanid	$$⊢\exists x\in z\left(x\in z\wedge \phi \right)\leftrightarrow \exists x\in z\phi$$
12	11	bibi2i	$$⊢\left(y\in w\leftrightarrow \exists x\in z\left(x\in z\wedge \phi \right)\right)\leftrightarrow \left(y\in w\leftrightarrow \exists x\in z\phi \right)$$
13	12	albii	$$⊢\forall y\left(y\in w\leftrightarrow \exists x\in z\left(x\in z\wedge \phi \right)\right)\leftrightarrow \forall y\left(y\in w\leftrightarrow \exists x\in z\phi \right)$$
14	13	exbii	$$⊢\exists w\forall y\left(y\in w\leftrightarrow \exists x\in z\left(x\in z\wedge \phi \right)\right)\leftrightarrow \exists w\forall y\left(y\in w\leftrightarrow \exists x\in z\phi \right)$$
15	10 14	sylib	$$⊢\forall x{\exists }^{*}y\left(x\in z\wedge \phi \right)\to \exists w\forall y\left(y\in w\leftrightarrow \exists x\in z\phi \right)$$
16	9 15	syl	$$⊢\forall x\in z\exists !y\phi \to \exists w\forall y\left(y\in w\leftrightarrow \exists x\in z\phi \right)$$
17		replem	$$⊢\left(\forall x\in z\exists y\phi \wedge \exists w\forall y\left(y\in w\leftrightarrow \exists x\in z\phi \right)\right)\to \exists w\forall x\in z\exists y\in w\phi$$
18	2 16 17	syl2anc	$$⊢\forall x\in z\exists !y\phi \to \exists w\forall x\in z\exists y\in w\phi$$