Theorem elirrv 8750

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 8758 and efrirr 5305, but this proof is direct from the Axiom of Regularity.) (Contributed by NM, 19-Aug-1993.)

Assertion

Ref	Expression
elirrv	⊢ ¬ 𝑥 ∈ 𝑥

Proof of Theorem elirrv

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

Step	Hyp	Ref	Expression
1		snex 5111	. . 3 ⊢ {𝑥} ∈ V
2		eleq1w 2879	. . . 4 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ {𝑥} ↔ 𝑥 ∈ {𝑥}))
3		vsnid 4414	. . . 4 ⊢ 𝑥 ∈ {𝑥}
4	2, 3	spei 2437	. . 3 ⊢ ∃𝑦 𝑦 ∈ {𝑥}
5		zfregcl 8748	. . 3 ⊢ ({𝑥} ∈ V → (∃𝑦 𝑦 ∈ {𝑥} → ∃𝑦 ∈ {𝑥}∀𝑧 ∈ 𝑦 ¬ 𝑧 ∈ {𝑥}))
6	1, 4, 5	mp2 9	. 2 ⊢ ∃𝑦 ∈ {𝑥}∀𝑧 ∈ 𝑦 ¬ 𝑧 ∈ {𝑥}
7		velsn 4397	. . . . . . 7 ⊢ (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥)
8		ax9 2170	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑥 → 𝑥 ∈ 𝑦))
9	8	equcoms 2117	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝑥 ∈ 𝑥 → 𝑥 ∈ 𝑦))
10	9	com12 32	. . . . . . 7 ⊢ (𝑥 ∈ 𝑥 → (𝑦 = 𝑥 → 𝑥 ∈ 𝑦))
11	7, 10	syl5bi 233	. . . . . 6 ⊢ (𝑥 ∈ 𝑥 → (𝑦 ∈ {𝑥} → 𝑥 ∈ 𝑦))
12		eleq1w 2879	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ {𝑥} ↔ 𝑥 ∈ {𝑥}))
13	12	notbid 309	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (¬ 𝑧 ∈ {𝑥} ↔ ¬ 𝑥 ∈ {𝑥}))
14	13	rspccv 3510	. . . . . . 7 ⊢ (∀𝑧 ∈ 𝑦 ¬ 𝑧 ∈ {𝑥} → (𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ {𝑥}))
15	3, 14	mt2i 134	. . . . . 6 ⊢ (∀𝑧 ∈ 𝑦 ¬ 𝑧 ∈ {𝑥} → ¬ 𝑥 ∈ 𝑦)
16	11, 15	nsyli 156	. . . . 5 ⊢ (𝑥 ∈ 𝑥 → (∀𝑧 ∈ 𝑦 ¬ 𝑧 ∈ {𝑥} → ¬ 𝑦 ∈ {𝑥}))
17	16	con2d 131	. . . 4 ⊢ (𝑥 ∈ 𝑥 → (𝑦 ∈ {𝑥} → ¬ ∀𝑧 ∈ 𝑦 ¬ 𝑧 ∈ {𝑥}))
18	17	ralrimiv 3164	. . 3 ⊢ (𝑥 ∈ 𝑥 → ∀𝑦 ∈ {𝑥} ¬ ∀𝑧 ∈ 𝑦 ¬ 𝑧 ∈ {𝑥})
19		ralnex 3191	. . 3 ⊢ (∀𝑦 ∈ {𝑥} ¬ ∀𝑧 ∈ 𝑦 ¬ 𝑧 ∈ {𝑥} ↔ ¬ ∃𝑦 ∈ {𝑥}∀𝑧 ∈ 𝑦 ¬ 𝑧 ∈ {𝑥})
20	18, 19	sylib 209	. 2 ⊢ (𝑥 ∈ 𝑥 → ¬ ∃𝑦 ∈ {𝑥}∀𝑧 ∈ 𝑦 ¬ 𝑧 ∈ {𝑥})
21	6, 20	mt2 191	1 ⊢ ¬ 𝑥 ∈ 𝑥

Syntax hints:  ¬ wn 3   → wi 4  ∃wex 1859   ∈ wcel 2157  ∀wral 3107  ∃wrex 3108  Vcvv 3402  {csn 4381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pr 5109  ax-reg 8746

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ral 3112  df-rex 3113  df-v 3404  df-dif 3783  df-un 3785  df-nul 4128  df-sn 4382  df-pr 4384

This theorem is referenced by:  elirr  8751  ruv  8756  dfac2OLD  9248  nd1  9704  nd2  9705  nd3  9706  axunnd  9713  axregndlem1  9719  axregndlem2  9720  axregnd  9721  elpotr  32028  exnel  32050  distel  32051