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 (see elirrvALT ), but this proof is direct from ax-reg . (Contributed by NM, 19-Aug-1993) Reduce axiom dependencies and make use of ax-reg directly. (Revised by BTernaryTau, 27-Dec-2025)

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

Proof

Step	Hyp	Ref	Expression
1		biimpr	$⊢ (y \in w \leftrightarrow y = x) \to (y = x \to y \in w)$
2	1	alimi	$⊢ \forall y (y \in w \leftrightarrow y = x) \to \forall y (y = x \to y \in w)$
3		elequ1	$⊢ y = x \to (y \in w \leftrightarrow x \in w)$
4	3	equsalvw	$⊢ \forall y (y = x \to y \in w) \leftrightarrow x \in w$
5	2 4	sylib	$⊢ \forall y (y \in w \leftrightarrow y = x) \to x \in w$
6	3	equsexvw	$⊢ \exists y (y = x \land y \in w) \leftrightarrow x \in w$
7		exsimpr	$⊢ \exists y (y = x \land y \in w) \to \exists y y \in w$
8	6 7	sylbir	$⊢ x \in w \to \exists y y \in w$
9		ax-reg	$⊢ \exists y y \in w \to \exists y (y \in w \land \forall z (z \in y \to \neg z \in w))$
10	8 9	syl	$⊢ x \in w \to \exists y (y \in w \land \forall z (z \in y \to \neg z \in w))$
11		elequ1	$⊢ z = x \to (z \in y \leftrightarrow x \in y)$
12		elequ1	$⊢ z = x \to (z \in w \leftrightarrow x \in w)$
13	12	notbid	$⊢ z = x \to (\neg z \in w \leftrightarrow \neg x \in w)$
14	11 13	imbi12d	$⊢ z = x \to ((z \in y \to \neg z \in w) \leftrightarrow (x \in y \to \neg x \in w))$
15	14	spvv	$⊢ \forall z (z \in y \to \neg z \in w) \to (x \in y \to \neg x \in w)$
16		con2	$⊢ (x \in y \to \neg x \in w) \to (x \in w \to \neg x \in y)$
17	16	com12	$⊢ x \in w \to ((x \in y \to \neg x \in w) \to \neg x \in y)$
18	17	anim2d	$⊢ x \in w \to ((y \in w \land (x \in y \to \neg x \in w)) \to (y \in w \land \neg x \in y))$
19	15 18	sylan2i	$⊢ x \in w \to ((y \in w \land \forall z (z \in y \to \neg z \in w)) \to (y \in w \land \neg x \in y))$
20	19	eximdv	$⊢ x \in w \to (\exists y (y \in w \land \forall z (z \in y \to \neg z \in w)) \to \exists y (y \in w \land \neg x \in y))$
21	10 20	mpd	$⊢ x \in w \to \exists y (y \in w \land \neg x \in y)$
22		19.29	$⊢ (\forall y (y \in w \leftrightarrow y = x) \land \exists y (y \in w \land \neg x \in y)) \to \exists y ((y \in w \leftrightarrow y = x) \land (y \in w \land \neg x \in y))$
23		biimp	$⊢ (y \in w \leftrightarrow y = x) \to (y \in w \to y = x)$
24	23	anim1d	$⊢ (y \in w \leftrightarrow y = x) \to ((y \in w \land \neg x \in y) \to (y = x \land \neg x \in y))$
25		ax9v2	$⊢ x = y \to (x \in x \to x \in y)$
26	25	equcoms	$⊢ y = x \to (x \in x \to x \in y)$
27	26	con3dimp	$⊢ (y = x \land \neg x \in y) \to \neg x \in x$
28	24 27	syl6	$⊢ (y \in w \leftrightarrow y = x) \to ((y \in w \land \neg x \in y) \to \neg x \in x)$
29	28	imp	$⊢ ((y \in w \leftrightarrow y = x) \land (y \in w \land \neg x \in y)) \to \neg x \in x$
30	29	exlimiv	$⊢ \exists y ((y \in w \leftrightarrow y = x) \land (y \in w \land \neg x \in y)) \to \neg x \in x$
31	22 30	syl	$⊢ (\forall y (y \in w \leftrightarrow y = x) \land \exists y (y \in w \land \neg x \in y)) \to \neg x \in x$
32	21 31	sylan2	$⊢ (\forall y (y \in w \leftrightarrow y = x) \land x \in w) \to \neg x \in x$
33	5 32	mpdan	$⊢ \forall y (y \in w \leftrightarrow y = x) \to \neg x \in x$
34		el	$⊢ \exists w x \in w$
35	4	biimpri	$⊢ x \in w \to \forall y (y = x \to y \in w)$
36	34 35	eximii	$⊢ \exists w \forall y (y = x \to y \in w)$
37	36	sepexi	$⊢ \exists w \forall y (y \in w \leftrightarrow y = x)$
38	33 37	exlimiiv	$⊢ \neg x \in x$

Metamath Proof Explorer

Theorem elirrv

Proof