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 (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	⊢ ¬ 𝑥 ∈ 𝑥

Proof

Step	Hyp	Ref	Expression
1		biimpr	⊢ ( ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) → ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑤 ) )
2	1	alimi	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) → ∀ 𝑦 ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑤 ) )
3		elequ1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝑤 ↔ 𝑥 ∈ 𝑤 ) )
4	3	equsalvw	⊢ ( ∀ 𝑦 ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑤 ) ↔ 𝑥 ∈ 𝑤 )
5	2 4	sylib	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) → 𝑥 ∈ 𝑤 )
6	3	equsexvw	⊢ ( ∃ 𝑦 ( 𝑦 = 𝑥 ∧ 𝑦 ∈ 𝑤 ) ↔ 𝑥 ∈ 𝑤 )
7		exsimpr	⊢ ( ∃ 𝑦 ( 𝑦 = 𝑥 ∧ 𝑦 ∈ 𝑤 ) → ∃ 𝑦 𝑦 ∈ 𝑤 )
8	6 7	sylbir	⊢ ( 𝑥 ∈ 𝑤 → ∃ 𝑦 𝑦 ∈ 𝑤 )
9		ax-reg	⊢ ( ∃ 𝑦 𝑦 ∈ 𝑤 → ∃ 𝑦 ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑤 ) ) )
10	8 9	syl	⊢ ( 𝑥 ∈ 𝑤 → ∃ 𝑦 ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑤 ) ) )
11		elequ1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦 ) )
12		elequ1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝑤 ↔ 𝑥 ∈ 𝑤 ) )
13	12	notbid	⊢ ( 𝑧 = 𝑥 → ( ¬ 𝑧 ∈ 𝑤 ↔ ¬ 𝑥 ∈ 𝑤 ) )
14	11 13	imbi12d	⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑤 ) ↔ ( 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑤 ) ) )
15	14	spvv	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑤 ) → ( 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑤 ) )
16		con2	⊢ ( ( 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑤 ) → ( 𝑥 ∈ 𝑤 → ¬ 𝑥 ∈ 𝑦 ) )
17	16	com12	⊢ ( 𝑥 ∈ 𝑤 → ( ( 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑤 ) → ¬ 𝑥 ∈ 𝑦 ) )
18	17	anim2d	⊢ ( 𝑥 ∈ 𝑤 → ( ( 𝑦 ∈ 𝑤 ∧ ( 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑤 ) ) → ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑦 ) ) )
19	15 18	sylan2i	⊢ ( 𝑥 ∈ 𝑤 → ( ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑤 ) ) → ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑦 ) ) )
20	19	eximdv	⊢ ( 𝑥 ∈ 𝑤 → ( ∃ 𝑦 ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑤 ) ) → ∃ 𝑦 ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑦 ) ) )
21	10 20	mpd	⊢ ( 𝑥 ∈ 𝑤 → ∃ 𝑦 ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑦 ) )
22		19.29	⊢ ( ( ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) ∧ ∃ 𝑦 ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑦 ) ) → ∃ 𝑦 ( ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑦 ) ) )
23		biimp	⊢ ( ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) → ( 𝑦 ∈ 𝑤 → 𝑦 = 𝑥 ) )
24	23	anim1d	⊢ ( ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) → ( ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑦 ) → ( 𝑦 = 𝑥 ∧ ¬ 𝑥 ∈ 𝑦 ) ) )
25		ax9v2	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑥 → 𝑥 ∈ 𝑦 ) )
26	25	equcoms	⊢ ( 𝑦 = 𝑥 → ( 𝑥 ∈ 𝑥 → 𝑥 ∈ 𝑦 ) )
27	26	con3dimp	⊢ ( ( 𝑦 = 𝑥 ∧ ¬ 𝑥 ∈ 𝑦 ) → ¬ 𝑥 ∈ 𝑥 )
28	24 27	syl6	⊢ ( ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) → ( ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑦 ) → ¬ 𝑥 ∈ 𝑥 ) )
29	28	imp	⊢ ( ( ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑦 ) ) → ¬ 𝑥 ∈ 𝑥 )
30	29	exlimiv	⊢ ( ∃ 𝑦 ( ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑦 ) ) → ¬ 𝑥 ∈ 𝑥 )
31	22 30	syl	⊢ ( ( ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) ∧ ∃ 𝑦 ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑦 ) ) → ¬ 𝑥 ∈ 𝑥 )
32	21 31	sylan2	⊢ ( ( ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) ∧ 𝑥 ∈ 𝑤 ) → ¬ 𝑥 ∈ 𝑥 )
33	5 32	mpdan	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) → ¬ 𝑥 ∈ 𝑥 )
34		el	⊢ ∃ 𝑤 𝑥 ∈ 𝑤
35	4	biimpri	⊢ ( 𝑥 ∈ 𝑤 → ∀ 𝑦 ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑤 ) )
36	34 35	eximii	⊢ ∃ 𝑤 ∀ 𝑦 ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑤 )
37	36	sepexi	⊢ ∃ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 )
38	33 37	exlimiiv	⊢ ¬ 𝑥 ∈ 𝑥