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

Theorem epel 4489
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 2951 . 2  |-  y  e. 
_V
21epelc 4488 1  |-  ( x  _E  y  <->  x  e.  y )
Colors of variables: wff set class
Syntax hints:    <-> wb 177   class class class wbr 4204    _E cep 4484
This theorem is referenced by:  epse  4557  dfepfr  4559  epfrc  4560  wecmpep  4566  wetrep  4567  ordon  4755  smoiso  6616  smoiso2  6623  ordunifi  7349  ordiso2  7476  ordtypelem8  7486  wofib  7506  dford2  7567  noinfep  7606  noinfepOLD  7607  oemapso  7630  wemapwe  7646  alephiso  7971  cflim2  8135  fin23lem27  8200  om2uzisoi  11286  efrunt  25154  dftr6  25365  dffr5  25368  elpotr  25400  dfon2lem9  25410  dfon2  25411  domep  25412  brsset  25726  dfon3  25729  brbigcup  25735  brapply  25775  brcup  25776  brcap  25777  tfrqfree  25788  dfint3  25789  bnj219  29037
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205  df-opab 4259  df-eprel 4486
  Copyright terms: Public domain W3C validator