Theorem elirrv 9506

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 9520 and efrirr 5600 (see elirrvALT 9521), but this proof is direct from ax-reg 9501. (Contributed by NM, 19-Aug-1993.) Reduce axiom dependencies and make use of ax-reg 9501 directly. (Revised by BTernaryTau, 27-Dec-2025.) Avoid ax-pr 5364. (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 2128	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝑥 ↔ 𝑥 ∈ 𝑥))
2	1	biimprcd 252	. . . . . . . 8 ⊢ (𝑥 ∈ 𝑥 → (𝑧 = 𝑥 → 𝑧 ∈ 𝑥))
3	2	pm4.71rd 568	. . . . . . 7 ⊢ (𝑥 ∈ 𝑥 → (𝑧 = 𝑥 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥)))
4	3	bibi2d 344	. . . . . 6 ⊢ (𝑥 ∈ 𝑥 → ((𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) ↔ (𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥))))
5	4	albidv 1928	. . . . 5 ⊢ (𝑥 ∈ 𝑥 → (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) ↔ ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥))))
6	5	biimprcd 252	. . . 4 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥)) → (𝑥 ∈ 𝑥 → ∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥)))
7		ax6ev 1977	. . . . . . . 8 ⊢ ∃𝑧 𝑧 = 𝑥
8		exbi 1855	. . . . . . . 8 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → (∃𝑧 𝑧 ∈ 𝑦 ↔ ∃𝑧 𝑧 = 𝑥))
9	7, 8	mpbiri 260	. . . . . . 7 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → ∃𝑧 𝑧 ∈ 𝑦)
10		ax-reg 9501	. . . . . . 7 ⊢ (∃𝑧 𝑧 ∈ 𝑦 → ∃𝑧(𝑧 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦)))
11	9, 10	syl 17	. . . . . 6 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → ∃𝑧(𝑧 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦)))
12		biimp 217	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → (𝑧 ∈ 𝑦 → 𝑧 = 𝑥))
13		elequ1 2128	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑧 ↔ 𝑧 ∈ 𝑧))
14		elequ1 2128	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦))
15	14	notbid 320	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (¬ 𝑥 ∈ 𝑦 ↔ ¬ 𝑧 ∈ 𝑦))
16	13, 15	imbi12d 346	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦) ↔ (𝑧 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑦)))
17	16	spvv 1996	. . . . . . . . . . 11 ⊢ (∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦) → (𝑧 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑦))
18	17	con2d 134	. . . . . . . . . 10 ⊢ (∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦) → (𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑧))
19	12, 18	anim12ii 625	. . . . . . . . 9 ⊢ (((𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) ∧ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦)) → (𝑧 ∈ 𝑦 → (𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧)))
20	19	ex 414	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → (∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦) → (𝑧 ∈ 𝑦 → (𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧))))
21	20	impcomd 413	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → ((𝑧 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦)) → (𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧)))
22	21	aleximi 1840	. . . . . 6 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → (∃𝑧(𝑧 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦)) → ∃𝑧(𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧)))
23	11, 22	mpd 15	. . . . 5 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → ∃𝑧(𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧))
24		elequ12 2139	. . . . . . . 8 ⊢ ((𝑧 = 𝑥 ∧ 𝑧 = 𝑥) → (𝑧 ∈ 𝑧 ↔ 𝑥 ∈ 𝑥))
25	24	anidms 572	. . . . . . 7 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝑧 ↔ 𝑥 ∈ 𝑥))
26	25	notbid 320	. . . . . 6 ⊢ (𝑧 = 𝑥 → (¬ 𝑧 ∈ 𝑧 ↔ ¬ 𝑥 ∈ 𝑥))
27	26	equsexvw 2013	. . . . 5 ⊢ (∃𝑧(𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧) ↔ ¬ 𝑥 ∈ 𝑥)
28	23, 27	sylib 220	. . . 4 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → ¬ 𝑥 ∈ 𝑥)
29	6, 28	syl6 35	. . 3 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥)) → (𝑥 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑥))
30	29	pm2.01d 191	. 2 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥)) → ¬ 𝑥 ∈ 𝑥)
31		axsepg 5221	. 2 ⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥))
32	30, 31	exlimiiv 1939	1 ⊢ ¬ 𝑥 ∈ 𝑥

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 397  ∀wal 1546  ∃wex 1787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-sep 5220  ax-reg 9501

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788

This theorem is referenced by:  elirr  9509  nd1  10506  nd2  10507  nd3  10508  axunnd  10515  axregndlem1  10521  axregndlem2  10522  axregnd  10523  axsepg2  35334  axsepg4  35337  axnulg  35339  axpowg2  35341  axpowg3  35342  elpotr  36020  exnel  36041  distel  36042  axtcond  36719  mh-setindnd  36778  ruvALT  43132  onsupmaxb  43697  ralndv1  47580