Theorem elirrv

Description: The membership relation is irreflexive: no set is a member of itself. Theorem 105 of Suppes p. 54. (This is trivial to prove from zfregfr and efrirr , but this proof is direct from the Axiom of Regularity.) (Contributed by NM, 19-Aug-1993)

	Ref	Expression
Assertion	elirrv	$$⊢\neg x\in x$$

Proof

Step	Hyp	Ref	Expression
1		vsnex	$$⊢\left\{x\right\}\in \mathrm{V}$$
2		eleq1w	$$⊢y=x\to \left(y\in \left\{x\right\}\leftrightarrow x\in \left\{x\right\}\right)$$
3		vsnid	$$⊢x\in \left\{x\right\}$$
4	2 3	speivw	$$⊢\exists yy\in \left\{x\right\}$$
5		zfregcl	$$⊢\left\{x\right\}\in \mathrm{V}\to \left(\exists yy\in \left\{x\right\}\to \exists y\in \left\{x\right\}\forall z\in y\neg z\in \left\{x\right\}\right)$$
6	1 4 5	mp2	$$⊢\exists y\in \left\{x\right\}\forall z\in y\neg z\in \left\{x\right\}$$
7		velsn	$$⊢y\in \left\{x\right\}\leftrightarrow y=x$$
8		ax9	$$⊢x=y\to \left(x\in x\to x\in y\right)$$
9	8	equcoms	$$⊢y=x\to \left(x\in x\to x\in y\right)$$
10	9	com12	$$⊢x\in x\to \left(y=x\to x\in y\right)$$
11	7 10	biimtrid	$$⊢x\in x\to \left(y\in \left\{x\right\}\to x\in y\right)$$
12		eleq1w	$$⊢z=x\to \left(z\in \left\{x\right\}\leftrightarrow x\in \left\{x\right\}\right)$$
13	12	notbid	$$⊢z=x\to \left(\neg z\in \left\{x\right\}\leftrightarrow \neg x\in \left\{x\right\}\right)$$
14	13	rspccv	$$⊢\forall z\in y\neg z\in \left\{x\right\}\to \left(x\in y\to \neg x\in \left\{x\right\}\right)$$
15	3 14	mt2i	$$⊢\forall z\in y\neg z\in \left\{x\right\}\to \neg x\in y$$
16	11 15	nsyli	$$⊢x\in x\to \left(\forall z\in y\neg z\in \left\{x\right\}\to \neg y\in \left\{x\right\}\right)$$
17	16	con2d	$$⊢x\in x\to \left(y\in \left\{x\right\}\to \neg \forall z\in y\neg z\in \left\{x\right\}\right)$$
18	17	ralrimiv	$$⊢x\in x\to \forall y\in \left\{x\right\}\neg \forall z\in y\neg z\in \left\{x\right\}$$
19		ralnex	$$⊢\forall y\in \left\{x\right\}\neg \forall z\in y\neg z\in \left\{x\right\}\leftrightarrow \neg \exists y\in \left\{x\right\}\forall z\in y\neg z\in \left\{x\right\}$$
20	18 19	sylib	$$⊢x\in x\to \neg \exists y\in \left\{x\right\}\forall z\in y\neg z\in \left\{x\right\}$$
21	6 20	mt2	$$⊢\neg x\in x$$