Theorem axrepndlem1

Description: Lemma for the Axiom of Replacement with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 2-Jan-2002) (New usage is discouraged.)

	Ref	Expression
Assertion	axrepndlem1	$$⊢\neg \forall yy=z\to \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 \forall y\phi \right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		axrep2	$$⊢\exists x\left(\exists y\forall w\left(\left[w/z\right]\phi \to w=y\right)\to \forall w\left(w\in x\leftrightarrow \exists x\left(x\in y\wedge \forall y\left[w/z\right]\phi \right)\right)\right)$$
2		nfnae	$$⊢Ⅎx\neg \forall yy=z$$
3		nfnae	$$⊢Ⅎy\neg \forall yy=z$$
4		nfnae	$$⊢Ⅎz\neg \forall yy=z$$
5		nfs1v	$$⊢Ⅎz\left[w/z\right]\phi$$
6	5	a1i	$$⊢\neg \forall yy=z\to Ⅎz\left[w/z\right]\phi$$
7		nfcvd	$$⊢\neg \forall yy=z\to \underset{\_}{Ⅎ}zw$$
8		nfcvf2	$$⊢\neg \forall yy=z\to \underset{\_}{Ⅎ}zy$$
9	7 8	nfeqd	$$⊢\neg \forall yy=z\to Ⅎzw=y$$
10	6 9	nfimd	$$⊢\neg \forall yy=z\to Ⅎz\left(\left[w/z\right]\phi \to w=y\right)$$
11		sbequ12r	$$⊢w=z\to \left(\left[w/z\right]\phi \leftrightarrow \phi \right)$$
12		equequ1	$$⊢w=z\to \left(w=y\leftrightarrow z=y\right)$$
13	11 12	imbi12d	$$⊢w=z\to \left(\left(\left[w/z\right]\phi \to w=y\right)\leftrightarrow \left(\phi \to z=y\right)\right)$$
14	13	a1i	$$⊢\neg \forall yy=z\to \left(w=z\to \left(\left(\left[w/z\right]\phi \to w=y\right)\leftrightarrow \left(\phi \to z=y\right)\right)\right)$$
15	4 10 14	cbvald	$$⊢\neg \forall yy=z\to \left(\forall w\left(\left[w/z\right]\phi \to w=y\right)\leftrightarrow \forall z\left(\phi \to z=y\right)\right)$$
16	3 15	exbid	$$⊢\neg \forall yy=z\to \left(\exists y\forall w\left(\left[w/z\right]\phi \to w=y\right)\leftrightarrow \exists y\forall z\left(\phi \to z=y\right)\right)$$
17		nfvd	$$⊢\neg \forall yy=z\to Ⅎzw\in x$$
18	8	nfcrd	$$⊢\neg \forall yy=z\to Ⅎzx\in y$$
19	3 6	nfald	$$⊢\neg \forall yy=z\to Ⅎz\forall y\left[w/z\right]\phi$$
20	18 19	nfand	$$⊢\neg \forall yy=z\to Ⅎz\left(x\in y\wedge \forall y\left[w/z\right]\phi \right)$$
21	2 20	nfexd	$$⊢\neg \forall yy=z\to Ⅎz\exists x\left(x\in y\wedge \forall y\left[w/z\right]\phi \right)$$
22	17 21	nfbid	$$⊢\neg \forall yy=z\to Ⅎz\left(w\in x\leftrightarrow \exists x\left(x\in y\wedge \forall y\left[w/z\right]\phi \right)\right)$$
23		elequ1	$$⊢w=z\to \left(w\in x\leftrightarrow z\in x\right)$$
24	23	adantl	$$⊢\left(\neg \forall yy=z\wedge w=z\right)\to \left(w\in x\leftrightarrow z\in x\right)$$
25		nfeqf2	$$⊢\neg \forall yy=z\to Ⅎyw=z$$
26	3 25	nfan1	$$⊢Ⅎy\left(\neg \forall yy=z\wedge w=z\right)$$
27	11	adantl	$$⊢\left(\neg \forall yy=z\wedge w=z\right)\to \left(\left[w/z\right]\phi \leftrightarrow \phi \right)$$
28	26 27	albid	$$⊢\left(\neg \forall yy=z\wedge w=z\right)\to \left(\forall y\left[w/z\right]\phi \leftrightarrow \forall y\phi \right)$$
29	28	anbi2d	$$⊢\left(\neg \forall yy=z\wedge w=z\right)\to \left(\left(x\in y\wedge \forall y\left[w/z\right]\phi \right)\leftrightarrow \left(x\in y\wedge \forall y\phi \right)\right)$$
30	29	exbidv	$$⊢\left(\neg \forall yy=z\wedge w=z\right)\to \left(\exists x\left(x\in y\wedge \forall y\left[w/z\right]\phi \right)\leftrightarrow \exists x\left(x\in y\wedge \forall y\phi \right)\right)$$
31	24 30	bibi12d	$$⊢\left(\neg \forall yy=z\wedge w=z\right)\to \left(\left(w\in x\leftrightarrow \exists x\left(x\in y\wedge \forall y\left[w/z\right]\phi \right)\right)\leftrightarrow \left(z\in x\leftrightarrow \exists x\left(x\in y\wedge \forall y\phi \right)\right)\right)$$
32	31	ex	$$⊢\neg \forall yy=z\to \left(w=z\to \left(\left(w\in x\leftrightarrow \exists x\left(x\in y\wedge \forall y\left[w/z\right]\phi \right)\right)\leftrightarrow \left(z\in x\leftrightarrow \exists x\left(x\in y\wedge \forall y\phi \right)\right)\right)\right)$$
33	4 22 32	cbvald	$$⊢\neg \forall yy=z\to \left(\forall w\left(w\in x\leftrightarrow \exists x\left(x\in y\wedge \forall y\left[w/z\right]\phi \right)\right)\leftrightarrow \forall z\left(z\in x\leftrightarrow \exists x\left(x\in y\wedge \forall y\phi \right)\right)\right)$$
34	16 33	imbi12d	$$⊢\neg \forall yy=z\to \left(\left(\exists y\forall w\left(\left[w/z\right]\phi \to w=y\right)\to \forall w\left(w\in x\leftrightarrow \exists x\left(x\in y\wedge \forall y\left[w/z\right]\phi \right)\right)\right)\leftrightarrow \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 \forall y\phi \right)\right)\right)\right)$$
35	2 34	exbid	$$⊢\neg \forall yy=z\to \left(\exists x\left(\exists y\forall w\left(\left[w/z\right]\phi \to w=y\right)\to \forall w\left(w\in x\leftrightarrow \exists x\left(x\in y\wedge \forall y\left[w/z\right]\phi \right)\right)\right)\leftrightarrow \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 \forall y\phi \right)\right)\right)\right)$$
36	1 35	mpbii	$$⊢\neg \forall yy=z\to \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 \forall y\phi \right)\right)\right)$$