Theorem elirrv 9591

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 9605 and efrirr 5630 (see elirrvALT 9606), but this proof is direct from ax-reg 9586. (Contributed by NM, 19-Aug-1993.) Reduce axiom dependencies and make use of ax-reg 9586 directly. (Revised by BTernaryTau, 27-Dec-2025.) Avoid ax-pr 5390. (Revised by BTernaryTau, 21-May-2026.) (Proof shortened by Matthew House, 23-May-2026.)

Assertion

Ref	Expression
elirrv	⊢ ¬ 𝑥 ∈ 𝑥

Proof of Theorem elirrv

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elequ1 2151	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝑥 ↔ 𝑥 ∈ 𝑥))
2	1	biimprcd 253	. . . . . . . 8 ⊢ (𝑥 ∈ 𝑥 → (𝑧 = 𝑥 → 𝑧 ∈ 𝑥))
3	2	pm4.71rd 572	. . . . . . 7 ⊢ (𝑥 ∈ 𝑥 → (𝑧 = 𝑥 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥)))
4	3	bibi2d 345	. . . . . 6 ⊢ (𝑥 ∈ 𝑥 → ((𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) ↔ (𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥))))
5	4	albidv 1952	. . . . 5 ⊢ (𝑥 ∈ 𝑥 → (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) ↔ ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥))))
6	5	biimprcd 253	. . . 4 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥)) → (𝑥 ∈ 𝑥 → ∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥)))
7		ax6ev 2001	. . . . . . . 8 ⊢ ∃𝑧 𝑧 = 𝑥
8		exbi 1879	. . . . . . . 8 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → (∃𝑧 𝑧 ∈ 𝑦 ↔ ∃𝑧 𝑧 = 𝑥))
9	7, 8	mpbiri 261	. . . . . . 7 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → ∃𝑧 𝑧 ∈ 𝑦)
10		ax-reg 9586	. . . . . . 7 ⊢ (∃𝑧 𝑧 ∈ 𝑦 → ∃𝑧(𝑧 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦)))
11	9, 10	syl 18	. . . . . 6 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → ∃𝑧(𝑧 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦)))
12		biimp 218	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → (𝑧 ∈ 𝑦 → 𝑧 = 𝑥))
13		elequ1 2151	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑧 ↔ 𝑧 ∈ 𝑧))
14		elequ1 2151	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦))
15	14	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (¬ 𝑥 ∈ 𝑦 ↔ ¬ 𝑧 ∈ 𝑦))
16	13, 15	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦) ↔ (𝑧 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑦)))
17	16	spvv 2020	. . . . . . . . . . 11 ⊢ (∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦) → (𝑧 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑦))
18	17	con2d 135	. . . . . . . . . 10 ⊢ (∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦) → (𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑧))
19	12, 18	anim12ii 630	. . . . . . . . 9 ⊢ (((𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) ∧ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦)) → (𝑧 ∈ 𝑦 → (𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧)))
20	19	ex 418	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → (∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦) → (𝑧 ∈ 𝑦 → (𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧))))
21	20	impcomd 417	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → ((𝑧 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦)) → (𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧)))
22	21	aleximi 1864	. . . . . 6 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → (∃𝑧(𝑧 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦)) → ∃𝑧(𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧)))
23	11, 22	mpd 16	. . . . 5 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → ∃𝑧(𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧))
24		elequ12 2162	. . . . . . . 8 ⊢ ((𝑧 = 𝑥 ∧ 𝑧 = 𝑥) → (𝑧 ∈ 𝑧 ↔ 𝑥 ∈ 𝑥))
25	24	anidms 577	. . . . . . 7 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝑧 ↔ 𝑥 ∈ 𝑥))
26	25	notbid 321	. . . . . 6 ⊢ (𝑧 = 𝑥 → (¬ 𝑧 ∈ 𝑧 ↔ ¬ 𝑥 ∈ 𝑥))
27	26	equsexvw 2037	. . . . 5 ⊢ (∃𝑧(𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧) ↔ ¬ 𝑥 ∈ 𝑥)
28	23, 27	sylib 221	. . . 4 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → ¬ 𝑥 ∈ 𝑥)
29	6, 28	syl6 36	. . 3 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥)) → (𝑥 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑥))
30	29	pm2.01d 192	. 2 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥)) → ¬ 𝑥 ∈ 𝑥)
31		axsepg 5249	. 2 ⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥))
32	30, 31	exlimiiv 1963	1 ⊢ ¬ 𝑥 ∈ 𝑥

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-sep 5248  ax-reg 9586

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812

This theorem is used by:  elirr  9594  nd1  10672  nd2  10673  nd3  10674  axunnd  10681  axregndlem1  10687  axregndlem2  10688  axregnd  10689  axsepg2  35808  axsepg4  35811  axnulg  35813  axpowg2  35815  axpowg3  35816  elpotr  36543  exnel  36564  distel  36565  axtcond  37266  mh-setindnd  37325  ruvALT  43681  onsupmaxb  44241  ralndv1  48175