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

Theorem elirrv 7512
 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 7517 and efrirr 4518, 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 eleq1 2461 . . . 4
2 vex 2916 . . . . 5
32snid 3798 . . . 4
41, 3spei 1964 . . 3
5 snex 4360 . . . 4
65zfregcl 7509 . . 3
74, 6ax-mp 8 . 2
8 elsn 3786 . . . . . . 7
9 ax-14 1725 . . . . . . . . 9
109equcoms 1689 . . . . . . . 8
1110com12 29 . . . . . . 7
128, 11syl5bi 209 . . . . . 6
13 eleq1 2461 . . . . . . . . 9
1413notbid 286 . . . . . . . 8
1514rspccv 3006 . . . . . . 7
163, 15mt2i 112 . . . . . 6
1712, 16nsyli 135 . . . . 5
1817con2d 109 . . . 4
1918ralrimiv 2745 . . 3
20 ralnex 2673 . . 3
2119, 20sylib 189 . 2
227, 21mt2 172 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4  wex 1547   wcel 1721  wral 2663  wrex 2664  csn 3771 This theorem is referenced by:  elirr  7513  ruv  7515  dfac2  7958  nd1  8409  nd2  8410  nd3  8411  axunnd  8418  axregndlem1  8424  axregndlem2  8425  axregnd  8426  elpotr  25320  exnel  25342  distel  25343 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-sep 4285  ax-nul 4293  ax-pr 4358  ax-reg 7507 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-ral 2668  df-rex 2669  df-v 2915  df-dif 3280  df-un 3282  df-nul 3586  df-sn 3777  df-pr 3778
 Copyright terms: Public domain W3C validator