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

Theorem epel 4766
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 3059 . 2  |-  y  e. 
_V
21epelc 4765 1  |-  ( x  _E  y  <->  x  e.  y )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189   class class class wbr 4415    _E cep 4761
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pr 4652
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-br 4416  df-opab 4475  df-eprel 4763
This theorem is referenced by:  epse  4835  dfepfr  4837  epfrc  4838  wecmpep  4844  wetrep  4845  ordon  6635  smoiso  7106  smoiso2  7113  ordunifi  7846  ordiso2  8055  ordtypelem8  8065  wofib  8085  dford2  8150  noinfep  8190  oemapso  8212  wemapwe  8227  alephiso  8554  cflim2  8718  fin23lem27  8783  om2uzisoi  12199  bnj219  29589  efrunt  30388  dftr6  30438  dffr5  30441  elpotr  30475  dfon2lem9  30485  dfon2  30486  domep  30487  brsset  30704  dfon3  30707  brbigcup  30713  brapply  30753  brcup  30754  brcap  30755  dfint3  30767
  Copyright terms: Public domain W3C validator