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

Theorem epel 4736
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 3061 . 2  |-  y  e. 
_V
21epelc 4735 1  |-  ( x  _E  y  <->  x  e.  y )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   class class class wbr 4394    _E cep 4731
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-br 4395  df-opab 4453  df-eprel 4733
This theorem is referenced by:  epse  4805  dfepfr  4807  epfrc  4808  wecmpep  4814  wetrep  4815  ordon  6556  smoiso  6990  smoiso2  6997  ordunifi  7724  ordiso2  7894  ordtypelem8  7904  wofib  7924  dford2  7990  noinfep  8029  oemapso  8053  wemapwe  8091  wemapweOLD  8092  alephiso  8431  cflim2  8595  fin23lem27  8660  om2uzisoi  12019  bnj219  28996  efrunt  29795  dftr6  29849  dffr5  29852  elpotr  29886  dfon2lem9  29896  dfon2  29897  domep  29898  brsset  30200  dfon3  30203  brbigcup  30209  brapply  30249  brcup  30250  brcap  30251  dfint3  30263
  Copyright terms: Public domain W3C validator