Theorem elirrv 9615

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 9629 and efrirr 5635 (see elirrvALT 9630), but this proof is direct from ax-reg 9610. (Contributed by NM, 19-Aug-1993.) Reduce axiom dependencies and make use of ax-reg 9610 directly. (Revised by BTernaryTau, 27-Dec-2025.) Avoid ax-pr 5395. (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 2154	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝑥 ↔ 𝑥 ∈ 𝑥))
2	1	biimprcd 253	. . . . . . . 8 ⊢ (𝑥 ∈ 𝑥 → (𝑧 = 𝑥 → 𝑧 ∈ 𝑥))
3	2	pm4.71rd 572	. . . . . . 7 ⊢ (𝑥 ∈ 𝑥 → (𝑧 = 𝑥 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥)))
4	3	bibi2d 345	. . . . . 6 ⊢ (𝑥 ∈ 𝑥 → ((𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) ↔ (𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥))))
5	4	albidv 1955	. . . . 5 ⊢ (𝑥 ∈ 𝑥 → (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) ↔ ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥))))
6	5	biimprcd 253	. . . 4 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥)) → (𝑥 ∈ 𝑥 → ∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥)))
7		ax6ev 2004	. . . . . . . 8 ⊢ ∃𝑧 𝑧 = 𝑥
8		exbi 1880	. . . . . . . 8 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → (∃𝑧 𝑧 ∈ 𝑦 ↔ ∃𝑧 𝑧 = 𝑥))
9	7, 8	mpbiri 261	. . . . . . 7 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → ∃𝑧 𝑧 ∈ 𝑦)
10		ax-reg 9610	. . . . . . 7 ⊢ (∃𝑧 𝑧 ∈ 𝑦 → ∃𝑧(𝑧 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦)))
11	9, 10	syl 18	. . . . . 6 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → ∃𝑧(𝑧 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦)))
12		biimp 218	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → (𝑧 ∈ 𝑦 → 𝑧 = 𝑥))
13		elequ1 2154	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑧 ↔ 𝑧 ∈ 𝑧))
14		elequ1 2154	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦))
15	14	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (¬ 𝑥 ∈ 𝑦 ↔ ¬ 𝑧 ∈ 𝑦))
16	13, 15	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦) ↔ (𝑧 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑦)))
17	16	spvv 2023	. . . . . . . . . . 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 1865	. . . . . 6 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → (∃𝑧(𝑧 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦)) → ∃𝑧(𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧)))
23	11, 22	mpd 16	. . . . 5 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → ∃𝑧(𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧))
24		elequ12 2165	. . . . . . . 8 ⊢ ((𝑧 = 𝑥 ∧ 𝑧 = 𝑥) → (𝑧 ∈ 𝑧 ↔ 𝑥 ∈ 𝑥))
25	24	anidms 577	. . . . . . 7 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝑧 ↔ 𝑥 ∈ 𝑥))
26	25	notbid 321	. . . . . 6 ⊢ (𝑧 = 𝑥 → (¬ 𝑧 ∈ 𝑧 ↔ ¬ 𝑥 ∈ 𝑥))
27	26	equsexvw 2040	. . . . 5 ⊢ (∃𝑧(𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧) ↔ ¬ 𝑥 ∈ 𝑥)
28	23, 27	sylib 221	. . . 4 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → ¬ 𝑥 ∈ 𝑥)
29	6, 28	syl6 36	. . 3 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥)) → (𝑥 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑥))
30	29	pm2.01d 192	. 2 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥)) → ¬ 𝑥 ∈ 𝑥)
31		axsepg 5253	. 2 ⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥))
32	30, 31	exlimiiv 1966	1 ⊢ ¬ 𝑥 ∈ 𝑥

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-sep 5252  ax-reg 9610

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

This theorem is used by:  elirr  9618  nd1  10696  nd2  10697  nd3  10698  axunnd  10705  axregndlem1  10711  axregndlem2  10712  axregnd  10713  axsepg2  35907  axsepg4  35910  axnulg  35912  axpowg2  35914  axpowg3  35915  elpotr  36720  exnel  36741  distel  36742  axtcond  37443  mh-setindnd  37502  ruvALT  43871  onsupmaxb  44431  ralndv1  48379