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) Avoid ax-pr . (Revised by BTernaryTau, 21-May-2026) (Proof shortened by Matthew House, 23-May-2026)

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

Proof

Step	Hyp	Ref	Expression
1		elequ1	$⊢ z = x \to (z \in x \leftrightarrow x \in x)$
2	1	biimprcd	$⊢ x \in x \to (z = x \to z \in x)$
3	2	pm4.71rd	$⊢ x \in x \to (z = x \leftrightarrow (z \in x \land z = x))$
4	3	bibi2d	$⊢ x \in x \to ((z \in y \leftrightarrow z = x) \leftrightarrow (z \in y \leftrightarrow (z \in x \land z = x)))$
5	4	albidv	$⊢ x \in x \to (\forall z (z \in y \leftrightarrow z = x) \leftrightarrow \forall z (z \in y \leftrightarrow (z \in x \land z = x)))$
6	5	biimprcd	$⊢ \forall z (z \in y \leftrightarrow (z \in x \land z = x)) \to (x \in x \to \forall z (z \in y \leftrightarrow z = x))$
7		ax6ev	$⊢ \exists z z = x$
8		exbi	$⊢ \forall z (z \in y \leftrightarrow z = x) \to (\exists z z \in y \leftrightarrow \exists z z = x)$
9	7 8	mpbiri	$⊢ \forall z (z \in y \leftrightarrow z = x) \to \exists z z \in y$
10		ax-reg	$⊢ \exists z z \in y \to \exists z (z \in y \land \forall x (x \in z \to \neg x \in y))$
11	9 10	syl	$⊢ \forall z (z \in y \leftrightarrow z = x) \to \exists z (z \in y \land \forall x (x \in z \to \neg x \in y))$
12		biimp	$⊢ (z \in y \leftrightarrow z = x) \to (z \in y \to z = x)$
13		elequ1	$⊢ x = z \to (x \in z \leftrightarrow z \in z)$
14		elequ1	$⊢ x = z \to (x \in y \leftrightarrow z \in y)$
15	14	notbid	$⊢ x = z \to (\neg x \in y \leftrightarrow \neg z \in y)$
16	13 15	imbi12d	$⊢ x = z \to ((x \in z \to \neg x \in y) \leftrightarrow (z \in z \to \neg z \in y))$
17	16	spvv	$⊢ \forall x (x \in z \to \neg x \in y) \to (z \in z \to \neg z \in y)$
18	17	con2d	$⊢ \forall x (x \in z \to \neg x \in y) \to (z \in y \to \neg z \in z)$
19	12 18	anim12ii	$⊢ ((z \in y \leftrightarrow z = x) \land \forall x (x \in z \to \neg x \in y)) \to (z \in y \to (z = x \land \neg z \in z))$
20	19	ex	$⊢ (z \in y \leftrightarrow z = x) \to (\forall x (x \in z \to \neg x \in y) \to (z \in y \to (z = x \land \neg z \in z)))$
21	20	impcomd	$⊢ (z \in y \leftrightarrow z = x) \to ((z \in y \land \forall x (x \in z \to \neg x \in y)) \to (z = x \land \neg z \in z))$
22	21	aleximi	$⊢ \forall z (z \in y \leftrightarrow z = x) \to (\exists z (z \in y \land \forall x (x \in z \to \neg x \in y)) \to \exists z (z = x \land \neg z \in z))$
23	11 22	mpd	$⊢ \forall z (z \in y \leftrightarrow z = x) \to \exists z (z = x \land \neg z \in z)$
24		elequ12	$⊢ (z = x \land z = x) \to (z \in z \leftrightarrow x \in x)$
25	24	anidms	$⊢ z = x \to (z \in z \leftrightarrow x \in x)$
26	25	notbid	$⊢ z = x \to (\neg z \in z \leftrightarrow \neg x \in x)$
27	26	equsexvw	$⊢ \exists z (z = x \land \neg z \in z) \leftrightarrow \neg x \in x$
28	23 27	sylib	$⊢ \forall z (z \in y \leftrightarrow z = x) \to \neg x \in x$
29	6 28	syl6	$⊢ \forall z (z \in y \leftrightarrow (z \in x \land z = x)) \to (x \in x \to \neg x \in x)$
30	29	pm2.01d	$⊢ \forall z (z \in y \leftrightarrow (z \in x \land z = x)) \to \neg x \in x$
31		axsepg	$⊢ \exists y \forall z (z \in y \leftrightarrow (z \in x \land z = x))$
32	30 31	exlimiiv	$⊢ \neg x \in x$

Metamath Proof Explorer

Theorem elirrv

Proof