MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elirrv Structured version   Visualization version   GIF version

Theorem elirrv 9637
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 9646 and efrirr 5664, 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.
StepHypRef Expression
1 vsnex 5433 . . 3 {𝑥} ∈ V
2 eleq1w 2823 . . . 4 (𝑦 = 𝑥 → (𝑦 ∈ {𝑥} ↔ 𝑥 ∈ {𝑥}))
3 vsnid 4662 . . . 4 𝑥 ∈ {𝑥}
42, 3speivw 1972 . . 3 𝑦 𝑦 ∈ {𝑥}
5 zfregcl 9635 . . 3 ({𝑥} ∈ V → (∃𝑦 𝑦 ∈ {𝑥} → ∃𝑦 ∈ {𝑥}∀𝑧𝑦 ¬ 𝑧 ∈ {𝑥}))
61, 4, 5mp2 9 . 2 𝑦 ∈ {𝑥}∀𝑧𝑦 ¬ 𝑧 ∈ {𝑥}
7 velsn 4641 . . . . . . 7 (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥)
8 ax9 2121 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑥𝑥𝑥𝑦))
98equcoms 2018 . . . . . . . 8 (𝑦 = 𝑥 → (𝑥𝑥𝑥𝑦))
109com12 32 . . . . . . 7 (𝑥𝑥 → (𝑦 = 𝑥𝑥𝑦))
117, 10biimtrid 242 . . . . . 6 (𝑥𝑥 → (𝑦 ∈ {𝑥} → 𝑥𝑦))
12 eleq1w 2823 . . . . . . . . 9 (𝑧 = 𝑥 → (𝑧 ∈ {𝑥} ↔ 𝑥 ∈ {𝑥}))
1312notbid 318 . . . . . . . 8 (𝑧 = 𝑥 → (¬ 𝑧 ∈ {𝑥} ↔ ¬ 𝑥 ∈ {𝑥}))
1413rspccv 3618 . . . . . . 7 (∀𝑧𝑦 ¬ 𝑧 ∈ {𝑥} → (𝑥𝑦 → ¬ 𝑥 ∈ {𝑥}))
153, 14mt2i 137 . . . . . 6 (∀𝑧𝑦 ¬ 𝑧 ∈ {𝑥} → ¬ 𝑥𝑦)
1611, 15nsyli 157 . . . . 5 (𝑥𝑥 → (∀𝑧𝑦 ¬ 𝑧 ∈ {𝑥} → ¬ 𝑦 ∈ {𝑥}))
1716con2d 134 . . . 4 (𝑥𝑥 → (𝑦 ∈ {𝑥} → ¬ ∀𝑧𝑦 ¬ 𝑧 ∈ {𝑥}))
1817ralrimiv 3144 . . 3 (𝑥𝑥 → ∀𝑦 ∈ {𝑥} ¬ ∀𝑧𝑦 ¬ 𝑧 ∈ {𝑥})
19 ralnex 3071 . . 3 (∀𝑦 ∈ {𝑥} ¬ ∀𝑧𝑦 ¬ 𝑧 ∈ {𝑥} ↔ ¬ ∃𝑦 ∈ {𝑥}∀𝑧𝑦 ¬ 𝑧 ∈ {𝑥})
2018, 19sylib 218 . 2 (𝑥𝑥 → ¬ ∃𝑦 ∈ {𝑥}∀𝑧𝑦 ¬ 𝑧 ∈ {𝑥})
216, 20mt2 200 1 ¬ 𝑥𝑥
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wex 1778  wcel 2107  wral 3060  wrex 3069  Vcvv 3479  {csn 4625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-pr 5431  ax-reg 9633
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-rex 3070  df-v 3481  df-un 3955  df-sn 4626  df-pr 4628
This theorem is referenced by:  elirr  9638  nd1  10628  nd2  10629  nd3  10630  axunnd  10637  axregndlem1  10643  axregndlem2  10644  axregnd  10645  axnulg  35107  elpotr  35783  exnel  35804  distel  35805  ruvALT  42684  onsupmaxb  43256  ralndv1  47122
  Copyright terms: Public domain W3C validator