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

	Ref	Expression
Assertion	elirrv	⊢ ¬ 𝑥 ∈ 𝑥

Proof

Step	Hyp	Ref	Expression
1		elequ1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝑥 ↔ 𝑥 ∈ 𝑥 ) )
2	1	biimprcd	⊢ ( 𝑥 ∈ 𝑥 → ( 𝑧 = 𝑥 → 𝑧 ∈ 𝑥 ) )
3	2	pm4.71rd	⊢ ( 𝑥 ∈ 𝑥 → ( 𝑧 = 𝑥 ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥 ) ) )
4	3	bibi2d	⊢ ( 𝑥 ∈ 𝑥 → ( ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) ↔ ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥 ) ) ) )
5	4	albidv	⊢ ( 𝑥 ∈ 𝑥 → ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥 ) ) ) )
6	5	biimprcd	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥 ) ) → ( 𝑥 ∈ 𝑥 → ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) ) )
7		ax6ev	⊢ ∃ 𝑧 𝑧 = 𝑥
8		exbi	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) → ( ∃ 𝑧 𝑧 ∈ 𝑦 ↔ ∃ 𝑧 𝑧 = 𝑥 ) )
9	7 8	mpbiri	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) → ∃ 𝑧 𝑧 ∈ 𝑦 )
10		ax-reg	⊢ ( ∃ 𝑧 𝑧 ∈ 𝑦 → ∃ 𝑧 ( 𝑧 ∈ 𝑦 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦 ) ) )
11	9 10	syl	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) → ∃ 𝑧 ( 𝑧 ∈ 𝑦 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦 ) ) )
12		biimp	⊢ ( ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) → ( 𝑧 ∈ 𝑦 → 𝑧 = 𝑥 ) )
13		elequ1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑧 ↔ 𝑧 ∈ 𝑧 ) )
14		elequ1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦 ) )
15	14	notbid	⊢ ( 𝑥 = 𝑧 → ( ¬ 𝑥 ∈ 𝑦 ↔ ¬ 𝑧 ∈ 𝑦 ) )
16	13 15	imbi12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦 ) ↔ ( 𝑧 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑦 ) ) )
17	16	spvv	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦 ) → ( 𝑧 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑦 ) )
18	17	con2d	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦 ) → ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑧 ) )
19	12 18	anim12ii	⊢ ( ( ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦 ) ) → ( 𝑧 ∈ 𝑦 → ( 𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧 ) ) )
20	19	ex	⊢ ( ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦 ) → ( 𝑧 ∈ 𝑦 → ( 𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧 ) ) ) )
21	20	impcomd	⊢ ( ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) → ( ( 𝑧 ∈ 𝑦 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦 ) ) → ( 𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧 ) ) )
22	21	aleximi	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) → ( ∃ 𝑧 ( 𝑧 ∈ 𝑦 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦 ) ) → ∃ 𝑧 ( 𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧 ) ) )
23	11 22	mpd	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) → ∃ 𝑧 ( 𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧 ) )
24		elequ12	⊢ ( ( 𝑧 = 𝑥 ∧ 𝑧 = 𝑥 ) → ( 𝑧 ∈ 𝑧 ↔ 𝑥 ∈ 𝑥 ) )
25	24	anidms	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝑧 ↔ 𝑥 ∈ 𝑥 ) )
26	25	notbid	⊢ ( 𝑧 = 𝑥 → ( ¬ 𝑧 ∈ 𝑧 ↔ ¬ 𝑥 ∈ 𝑥 ) )
27	26	equsexvw	⊢ ( ∃ 𝑧 ( 𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧 ) ↔ ¬ 𝑥 ∈ 𝑥 )
28	23 27	sylib	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) → ¬ 𝑥 ∈ 𝑥 )
29	6 28	syl6	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥 ) ) → ( 𝑥 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑥 ) )
30	29	pm2.01d	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥 ) ) → ¬ 𝑥 ∈ 𝑥 )
31		axsepg	⊢ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥 ) )
32	30 31	exlimiiv	⊢ ¬ 𝑥 ∈ 𝑥