Theorem axrep1

Description: The version of the Axiom of Replacement used in the Metamath Solitaire applet https://us.metamath.org/mmsolitaire/mms.html . Equivalence is shown via the path ax-rep -> axrep1 -> axrep2 -> axrepnd -> zfcndrep = ax-rep . (Contributed by NM, 19-Nov-2005) (Proof shortened by Mario Carneiro, 17-Nov-2016) Remove dependency on ax-13 . (Revised by BJ, 31-May-2019)

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

Proof

Step	Hyp	Ref	Expression
1		elequ2	$$⊢w=y\to \left(x\in w\leftrightarrow x\in y\right)$$
2	1	anbi1d	$$⊢w=y\to \left(\left(x\in w\wedge \phi \right)\leftrightarrow \left(x\in y\wedge \phi \right)\right)$$
3	2	exbidv	$$⊢w=y\to \left(\exists x\left(x\in w\wedge \phi \right)\leftrightarrow \exists x\left(x\in y\wedge \phi \right)\right)$$
4	3	bibi2d	$$⊢w=y\to \left(\left(z\in x\leftrightarrow \exists x\left(x\in w\wedge \phi \right)\right)\leftrightarrow \left(z\in x\leftrightarrow \exists x\left(x\in y\wedge \phi \right)\right)\right)$$
5	4	albidv	$$⊢w=y\to \left(\forall z\left(z\in x\leftrightarrow \exists x\left(x\in w\wedge \phi \right)\right)\leftrightarrow \forall z\left(z\in x\leftrightarrow \exists x\left(x\in y\wedge \phi \right)\right)\right)$$
6	5	exbidv	$$⊢w=y\to \left(\exists x\forall z\left(z\in x\leftrightarrow \exists x\left(x\in w\wedge \phi \right)\right)\leftrightarrow \exists x\forall z\left(z\in x\leftrightarrow \exists x\left(x\in y\wedge \phi \right)\right)\right)$$
7	6	imbi2d	$$⊢w=y\to \left(\left(\forall x\exists y\forall z\left(\phi \to z=y\right)\to \exists x\forall z\left(z\in x\leftrightarrow \exists x\left(x\in w\wedge \phi \right)\right)\right)\leftrightarrow \left(\forall x\exists y\forall z\left(\phi \to z=y\right)\to \exists x\forall z\left(z\in x\leftrightarrow \exists x\left(x\in y\wedge \phi \right)\right)\right)\right)$$
8		ax-rep	$$⊢\forall x\exists y\forall z\left(\forall y\phi \to z=y\right)\to \exists y\forall z\left(z\in y\leftrightarrow \exists x\left(x\in w\wedge \forall y\phi \right)\right)$$
9		19.3v	$$⊢\forall y\phi \leftrightarrow \phi$$
10	9	imbi1i	$$⊢\left(\forall y\phi \to z=y\right)\leftrightarrow \left(\phi \to z=y\right)$$
11	10	albii	$$⊢\forall z\left(\forall y\phi \to z=y\right)\leftrightarrow \forall z\left(\phi \to z=y\right)$$
12	11	exbii	$$⊢\exists y\forall z\left(\forall y\phi \to z=y\right)\leftrightarrow \exists y\forall z\left(\phi \to z=y\right)$$
13	12	albii	$$⊢\forall x\exists y\forall z\left(\forall y\phi \to z=y\right)\leftrightarrow \forall x\exists y\forall z\left(\phi \to z=y\right)$$
14		nfv	$$⊢Ⅎxz\in y$$
15		nfe1	$$⊢Ⅎx\exists x\left(x\in w\wedge \forall y\phi \right)$$
16	14 15	nfbi	$$⊢Ⅎx\left(z\in y\leftrightarrow \exists x\left(x\in w\wedge \forall y\phi \right)\right)$$
17	16	nfal	$$⊢Ⅎx\forall z\left(z\in y\leftrightarrow \exists x\left(x\in w\wedge \forall y\phi \right)\right)$$
18		nfv	$$⊢Ⅎy\forall z\left(z\in x\leftrightarrow \exists x\left(x\in w\wedge \phi \right)\right)$$
19		elequ2	$$⊢y=x\to \left(z\in y\leftrightarrow z\in x\right)$$
20	9	anbi2i	$$⊢\left(x\in w\wedge \forall y\phi \right)\leftrightarrow \left(x\in w\wedge \phi \right)$$
21	20	exbii	$$⊢\exists x\left(x\in w\wedge \forall y\phi \right)\leftrightarrow \exists x\left(x\in w\wedge \phi \right)$$
22	21	a1i	$$⊢y=x\to \left(\exists x\left(x\in w\wedge \forall y\phi \right)\leftrightarrow \exists x\left(x\in w\wedge \phi \right)\right)$$
23	19 22	bibi12d	$$⊢y=x\to \left(\left(z\in y\leftrightarrow \exists x\left(x\in w\wedge \forall y\phi \right)\right)\leftrightarrow \left(z\in x\leftrightarrow \exists x\left(x\in w\wedge \phi \right)\right)\right)$$
24	23	albidv	$$⊢y=x\to \left(\forall z\left(z\in y\leftrightarrow \exists x\left(x\in w\wedge \forall y\phi \right)\right)\leftrightarrow \forall z\left(z\in x\leftrightarrow \exists x\left(x\in w\wedge \phi \right)\right)\right)$$
25	17 18 24	cbvexv1	$$⊢\exists y\forall z\left(z\in y\leftrightarrow \exists x\left(x\in w\wedge \forall y\phi \right)\right)\leftrightarrow \exists x\forall z\left(z\in x\leftrightarrow \exists x\left(x\in w\wedge \phi \right)\right)$$
26	8 13 25	3imtr3i	$$⊢\forall x\exists y\forall z\left(\phi \to z=y\right)\to \exists x\forall z\left(z\in x\leftrightarrow \exists x\left(x\in w\wedge \phi \right)\right)$$
27	7 26	chvarvv	$$⊢\forall x\exists y\forall z\left(\phi \to z=y\right)\to \exists x\forall z\left(z\in x\leftrightarrow \exists x\left(x\in y\wedge \phi \right)\right)$$
28	27	19.35ri	$$⊢\exists x\left(\exists y\forall z\left(\phi \to z=y\right)\to \forall z\left(z\in x\leftrightarrow \exists x\left(x\in y\wedge \phi \right)\right)\right)$$