Theorem axregnd

Description: A version of the Axiom of Regularity with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 3-Jan-2002) (Proof shortened by Wolf Lammen, 18-Aug-2019) (New usage is discouraged.)

	Ref	Expression
Assertion	axregnd	$$⊢x\in y\to \exists x\left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		axregndlem2	$$⊢x\in y\to \exists x\left(x\in y\wedge \forall w\left(w\in x\to \neg w\in y\right)\right)$$
2		nfnae	$$⊢Ⅎx\neg \forall zz=x$$
3		nfnae	$$⊢Ⅎx\neg \forall zz=y$$
4	2 3	nfan	$$⊢Ⅎx\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)$$
5		nfnae	$$⊢Ⅎz\neg \forall zz=x$$
6		nfnae	$$⊢Ⅎz\neg \forall zz=y$$
7	5 6	nfan	$$⊢Ⅎz\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)$$
8		nfcvf	$$⊢\neg \forall zz=x\to \underset{\_}{Ⅎ}zx$$
9	8	nfcrd	$$⊢\neg \forall zz=x\to Ⅎzw\in x$$
10	9	adantr	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to Ⅎzw\in x$$
11		nfcvf	$$⊢\neg \forall zz=y\to \underset{\_}{Ⅎ}zy$$
12	11	nfcrd	$$⊢\neg \forall zz=y\to Ⅎzw\in y$$
13	12	nfnd	$$⊢\neg \forall zz=y\to Ⅎz\neg w\in y$$
14	13	adantl	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to Ⅎz\neg w\in y$$
15	10 14	nfimd	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to Ⅎz\left(w\in x\to \neg w\in y\right)$$
16		elequ1	$$⊢w=z\to \left(w\in x\leftrightarrow z\in x\right)$$
17		elequ1	$$⊢w=z\to \left(w\in y\leftrightarrow z\in y\right)$$
18	17	notbid	$$⊢w=z\to \left(\neg w\in y\leftrightarrow \neg z\in y\right)$$
19	16 18	imbi12d	$$⊢w=z\to \left(\left(w\in x\to \neg w\in y\right)\leftrightarrow \left(z\in x\to \neg z\in y\right)\right)$$
20	19	a1i	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to \left(w=z\to \left(\left(w\in x\to \neg w\in y\right)\leftrightarrow \left(z\in x\to \neg z\in y\right)\right)\right)$$
21	7 15 20	cbvald	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to \left(\forall w\left(w\in x\to \neg w\in y\right)\leftrightarrow \forall z\left(z\in x\to \neg z\in y\right)\right)$$
22	21	anbi2d	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to \left(\left(x\in y\wedge \forall w\left(w\in x\to \neg w\in y\right)\right)\leftrightarrow \left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)\right)$$
23	4 22	exbid	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to \left(\exists x\left(x\in y\wedge \forall w\left(w\in x\to \neg w\in y\right)\right)\leftrightarrow \exists x\left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)\right)$$
24	1 23	syl5ib	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to \left(x\in y\to \exists x\left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)\right)$$
25	24	ex	$$⊢\neg \forall zz=x\to \left(\neg \forall zz=y\to \left(x\in y\to \exists x\left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)\right)\right)$$
26		axregndlem1	$$⊢\forall xx=z\to \left(x\in y\to \exists x\left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)\right)$$
27	26	aecoms	$$⊢\forall zz=x\to \left(x\in y\to \exists x\left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)\right)$$
28		19.8a	$$⊢x\in y\to \exists xx\in y$$
29		nfae	$$⊢Ⅎx\forall zz=y$$
30		elirrv	$$⊢\neg z\in z$$
31		elequ2	$$⊢z=y\to \left(z\in z\leftrightarrow z\in y\right)$$
32	30 31	mtbii	$$⊢z=y\to \neg z\in y$$
33	32	a1d	$$⊢z=y\to \left(z\in x\to \neg z\in y\right)$$
34	33	alimi	$$⊢\forall zz=y\to \forall z\left(z\in x\to \neg z\in y\right)$$
35	34	anim2i	$$⊢\left(x\in y\wedge \forall zz=y\right)\to \left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)$$
36	35	expcom	$$⊢\forall zz=y\to \left(x\in y\to \left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)\right)$$
37	29 36	eximd	$$⊢\forall zz=y\to \left(\exists xx\in y\to \exists x\left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)\right)$$
38	28 37	syl5	$$⊢\forall zz=y\to \left(x\in y\to \exists x\left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)\right)$$
39	25 27 38	pm2.61ii	$$⊢x\in y\to \exists x\left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)$$