Theorem elirrv 9557

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 9571 and efrirr 5640 (see elirrvALT 9572), but this proof is direct from ax-reg 9552. (Contributed by NM, 19-Aug-1993.) Reduce axiom dependencies and make use of ax-reg 9552 directly. (Revised by BTernaryTau, 27-Dec-2025.) Avoid ax-pr 5403. (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 2149	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝑥 ↔ 𝑥 ∈ 𝑥))
2	1	biimprcd 253	. . . . . . . 8 ⊢ (𝑥 ∈ 𝑥 → (𝑧 = 𝑥 → 𝑧 ∈ 𝑥))
3	2	pm4.71rd 571	. . . . . . 7 ⊢ (𝑥 ∈ 𝑥 → (𝑧 = 𝑥 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥)))
4	3	bibi2d 345	. . . . . 6 ⊢ (𝑥 ∈ 𝑥 → ((𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) ↔ (𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥))))
5	4	albidv 1949	. . . . 5 ⊢ (𝑥 ∈ 𝑥 → (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) ↔ ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥))))
6	5	biimprcd 253	. . . 4 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥)) → (𝑥 ∈ 𝑥 → ∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥)))
7		ax6ev 1998	. . . . . . . 8 ⊢ ∃𝑧 𝑧 = 𝑥
8		exbi 1876	. . . . . . . 8 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → (∃𝑧 𝑧 ∈ 𝑦 ↔ ∃𝑧 𝑧 = 𝑥))
9	7, 8	mpbiri 261	. . . . . . 7 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → ∃𝑧 𝑧 ∈ 𝑦)
10		ax-reg 9552	. . . . . . 7 ⊢ (∃𝑧 𝑧 ∈ 𝑦 → ∃𝑧(𝑧 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦)))
11	9, 10	syl 18	. . . . . 6 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → ∃𝑧(𝑧 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦)))
12		biimp 218	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → (𝑧 ∈ 𝑦 → 𝑧 = 𝑥))
13		elequ1 2149	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑧 ↔ 𝑧 ∈ 𝑧))
14		elequ1 2149	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦))
15	14	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (¬ 𝑥 ∈ 𝑦 ↔ ¬ 𝑧 ∈ 𝑦))
16	13, 15	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦) ↔ (𝑧 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑦)))
17	16	spvv 2017	. . . . . . . . . . 11 ⊢ (∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦) → (𝑧 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑦))
18	17	con2d 135	. . . . . . . . . 10 ⊢ (∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦) → (𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑧))
19	12, 18	anim12ii 629	. . . . . . . . 9 ⊢ (((𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) ∧ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦)) → (𝑧 ∈ 𝑦 → (𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧)))
20	19	ex 417	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → (∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦) → (𝑧 ∈ 𝑦 → (𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧))))
21	20	impcomd 416	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → ((𝑧 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦)) → (𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧)))
22	21	aleximi 1861	. . . . . 6 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → (∃𝑧(𝑧 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦)) → ∃𝑧(𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧)))
23	11, 22	mpd 16	. . . . 5 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → ∃𝑧(𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧))
24		elequ12 2160	. . . . . . . 8 ⊢ ((𝑧 = 𝑥 ∧ 𝑧 = 𝑥) → (𝑧 ∈ 𝑧 ↔ 𝑥 ∈ 𝑥))
25	24	anidms 576	. . . . . . 7 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝑧 ↔ 𝑥 ∈ 𝑥))
26	25	notbid 321	. . . . . 6 ⊢ (𝑧 = 𝑥 → (¬ 𝑧 ∈ 𝑧 ↔ ¬ 𝑥 ∈ 𝑥))
27	26	equsexvw 2034	. . . . 5 ⊢ (∃𝑧(𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧) ↔ ¬ 𝑥 ∈ 𝑥)
28	23, 27	sylib 221	. . . 4 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → ¬ 𝑥 ∈ 𝑥)
29	6, 28	syl6 36	. . 3 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥)) → (𝑥 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑥))
30	29	pm2.01d 192	. 2 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥)) → ¬ 𝑥 ∈ 𝑥)
31		axsepg 5257	. 2 ⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥))
32	30, 31	exlimiiv 1960	1 ⊢ ¬ 𝑥 ∈ 𝑥

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-sep 5256  ax-reg 9552

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809

This theorem is used by:  elirr  9560  nd1  10578  nd2  10579  nd3  10580  axunnd  10587  axregndlem1  10593  axregndlem2  10594  axregnd  10595  axsepg2  35561  axsepg4  35564  axnulg  35566  axpowg2  35568  axpowg3  35569  elpotr  36279  exnel  36300  distel  36301  axtcond  37017  mh-setindnd  37076  ruvALT  43429  onsupmaxb  43994  ralndv1  47870