Theorem elirrv 9547

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 9561 and efrirr 5629 (see elirrvALT 9562), but this proof is direct from ax-reg 9542. (Contributed by NM, 19-Aug-1993.) Reduce axiom dependencies and make use of ax-reg 9542 directly. (Revised by BTernaryTau, 27-Dec-2025.) Avoid ax-pr 5392. (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 252	. . . . . . . 8 ⊢ (𝑥 ∈ 𝑥 → (𝑧 = 𝑥 → 𝑧 ∈ 𝑥))
3	2	pm4.71rd 570	. . . . . . 7 ⊢ (𝑥 ∈ 𝑥 → (𝑧 = 𝑥 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥)))
4	3	bibi2d 344	. . . . . 6 ⊢ (𝑥 ∈ 𝑥 → ((𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) ↔ (𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥))))
5	4	albidv 1942	. . . . 5 ⊢ (𝑥 ∈ 𝑥 → (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) ↔ ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥))))
6	5	biimprcd 252	. . . 4 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥)) → (𝑥 ∈ 𝑥 → ∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥)))
7		ax6ev 1991	. . . . . . . 8 ⊢ ∃𝑧 𝑧 = 𝑥
8		exbi 1869	. . . . . . . 8 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → (∃𝑧 𝑧 ∈ 𝑦 ↔ ∃𝑧 𝑧 = 𝑥))
9	7, 8	mpbiri 260	. . . . . . 7 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → ∃𝑧 𝑧 ∈ 𝑦)
10		ax-reg 9542	. . . . . . 7 ⊢ (∃𝑧 𝑧 ∈ 𝑦 → ∃𝑧(𝑧 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦)))
11	9, 10	syl 17	. . . . . 6 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → ∃𝑧(𝑧 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦)))
12		biimp 217	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → (𝑧 ∈ 𝑦 → 𝑧 = 𝑥))
13		elequ1 2151	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑧 ↔ 𝑧 ∈ 𝑧))
14		elequ1 2151	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦))
15	14	notbid 320	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (¬ 𝑥 ∈ 𝑦 ↔ ¬ 𝑧 ∈ 𝑦))
16	13, 15	imbi12d 346	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦) ↔ (𝑧 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑦)))
17	16	spvv 2010	. . . . . . . . . . 11 ⊢ (∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦) → (𝑧 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑦))
18	17	con2d 134	. . . . . . . . . 10 ⊢ (∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦) → (𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑧))
19	12, 18	anim12ii 627	. . . . . . . . 9 ⊢ (((𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) ∧ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦)) → (𝑧 ∈ 𝑦 → (𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧)))
20	19	ex 416	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → (∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦) → (𝑧 ∈ 𝑦 → (𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧))))
21	20	impcomd 415	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → ((𝑧 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦)) → (𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧)))
22	21	aleximi 1854	. . . . . 6 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → (∃𝑧(𝑧 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦)) → ∃𝑧(𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧)))
23	11, 22	mpd 15	. . . . 5 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → ∃𝑧(𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧))
24		elequ12 2162	. . . . . . . 8 ⊢ ((𝑧 = 𝑥 ∧ 𝑧 = 𝑥) → (𝑧 ∈ 𝑧 ↔ 𝑥 ∈ 𝑥))
25	24	anidms 574	. . . . . . 7 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝑧 ↔ 𝑥 ∈ 𝑥))
26	25	notbid 320	. . . . . 6 ⊢ (𝑧 = 𝑥 → (¬ 𝑧 ∈ 𝑧 ↔ ¬ 𝑥 ∈ 𝑥))
27	26	equsexvw 2027	. . . . 5 ⊢ (∃𝑧(𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧) ↔ ¬ 𝑥 ∈ 𝑥)
28	23, 27	sylib 220	. . . 4 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) → ¬ 𝑥 ∈ 𝑥)
29	6, 28	syl6 35	. . 3 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥)) → (𝑥 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑥))
30	29	pm2.01d 191	. 2 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥)) → ¬ 𝑥 ∈ 𝑥)
31		axsepg 5249	. 2 ⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥))
32	30, 31	exlimiiv 1953	1 ⊢ ¬ 𝑥 ∈ 𝑥

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399  ∀wal 1560  ∃wex 1801

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-sep 5248  ax-reg 9542

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802

This theorem is referenced by:  elirr  9550  nd1  10547  nd2  10548  nd3  10549  axunnd  10556  axregndlem1  10562  axregndlem2  10563  axregnd  10564  axsepg2  35440  axsepg4  35443  axnulg  35445  axpowg2  35447  axpowg3  35448  elpotr  36134  exnel  36155  distel  36156  axtcond  36843  mh-setindnd  36902  ruvALT  43256  onsupmaxb  43821  ralndv1  47704