Theorem distel

Description: Distinctors in terms of membership. (NOTE: this only works with relations where we can prove el and elirrv .) (Contributed by Scott Fenton, 15-Dec-2010)

	Ref	Expression
Assertion	distel	$$⊢\neg \forall yy=x\leftrightarrow \neg \forall y\neg x\in y$$

Proof

Step	Hyp	Ref	Expression
1		el	$$⊢\exists zx\in z$$
2		df-ex	$$⊢\exists zx\in z\leftrightarrow \neg \forall z\neg x\in z$$
3		nfnae	$$⊢Ⅎy\neg \forall yy=x$$
4		dveel1	$$⊢\neg \forall yy=x\to \left(x\in z\to \forall yx\in z\right)$$
5	3 4	nf5d	$$⊢\neg \forall yy=x\to Ⅎyx\in z$$
6	5	nfnd	$$⊢\neg \forall yy=x\to Ⅎy\neg x\in z$$
7		elequ2	$$⊢z=y\to \left(x\in z\leftrightarrow x\in y\right)$$
8	7	notbid	$$⊢z=y\to \left(\neg x\in z\leftrightarrow \neg x\in y\right)$$
9	8	a1i	$$⊢\neg \forall yy=x\to \left(z=y\to \left(\neg x\in z\leftrightarrow \neg x\in y\right)\right)$$
10	3 6 9	cbvald	$$⊢\neg \forall yy=x\to \left(\forall z\neg x\in z\leftrightarrow \forall y\neg x\in y\right)$$
11	10	notbid	$$⊢\neg \forall yy=x\to \left(\neg \forall z\neg x\in z\leftrightarrow \neg \forall y\neg x\in y\right)$$
12	2 11	bitrid	$$⊢\neg \forall yy=x\to \left(\exists zx\in z\leftrightarrow \neg \forall y\neg x\in y\right)$$
13	1 12	mpbii	$$⊢\neg \forall yy=x\to \neg \forall y\neg x\in y$$
14		elirrv	$$⊢\neg y\in y$$
15		elequ1	$$⊢y=x\to \left(y\in y\leftrightarrow x\in y\right)$$
16	14 15	mtbii	$$⊢y=x\to \neg x\in y$$
17	16	alimi	$$⊢\forall yy=x\to \forall y\neg x\in y$$
18	17	con3i	$$⊢\neg \forall y\neg x\in y\to \neg \forall yy=x$$
19	13 18	impbii	$$⊢\neg \forall yy=x\leftrightarrow \neg \forall y\neg x\in y$$