Theorem bj-rep

Description: Version of the axiom of replacement requiring the functional relation in the axiom to be a (total) function from ax-rep (in the form of axrep6 ). (Contributed by BJ, 14-Mar-2026) (Proof modification is discouraged.) (New usage is discouraded.)

	Ref	Expression
Assertion	bj-rep	$$⊢\forall x\left(\forall y\in x\exists !z\phi \to \exists t\forall z\left(z\in t\leftrightarrow \exists y\in x\phi \right)\right)$$

Proof

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