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

Theorem epel 4789
Description: The epsilon relation and the membership relation are the same. (Contributed by NM, 13-Aug-1995.)
Assertion
Ref Expression
epel  |-  ( x  _E  y  <->  x  e.  y )

Proof of Theorem epel
StepHypRef Expression
1 vex 3111 . 2  |-  y  e. 
_V
21epelc 4788 1  |-  ( x  _E  y  <->  x  e.  y )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   class class class wbr 4442    _E cep 4784
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-sep 4563  ax-nul 4571  ax-pr 4681
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2274  df-mo 2275  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-rab 2818  df-v 3110  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-br 4443  df-opab 4501  df-eprel 4786
This theorem is referenced by:  epse  4857  dfepfr  4859  epfrc  4860  wecmpep  4866  wetrep  4867  ordon  6591  smoiso  7025  smoiso2  7032  ordunifi  7761  ordiso2  7931  ordtypelem8  7941  wofib  7961  dford2  8028  noinfep  8067  noinfepOLD  8068  oemapso  8092  wemapwe  8130  wemapweOLD  8131  alephiso  8470  cflim2  8634  fin23lem27  8699  om2uzisoi  12023  efrunt  28548  dftr6  28744  dffr5  28747  elpotr  28778  dfon2lem9  28788  dfon2  28789  domep  28790  brsset  29104  dfon3  29107  brbigcup  29113  brapply  29153  brcup  29154  brcap  29155  tfrqfree  29166  dfint3  29167  bnj219  32745
  Copyright terms: Public domain W3C validator