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

Theorem epel 4765
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 3085 . 2  |-  y  e. 
_V
21epelc 4764 1  |-  ( x  _E  y  <->  x  e.  y )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188   class class class wbr 4421    _E cep 4760
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pr 4658
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-rab 2785  df-v 3084  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-br 4422  df-opab 4481  df-eprel 4762
This theorem is referenced by:  epse  4834  dfepfr  4836  epfrc  4837  wecmpep  4843  wetrep  4844  ordon  6621  smoiso  7087  smoiso2  7094  ordunifi  7825  ordiso2  8034  ordtypelem8  8044  wofib  8064  dford2  8129  noinfep  8168  oemapso  8190  wemapwe  8205  alephiso  8531  cflim2  8695  fin23lem27  8760  om2uzisoi  12169  bnj219  29543  efrunt  30342  dftr6  30391  dffr5  30394  elpotr  30428  dfon2lem9  30438  dfon2  30439  domep  30440  brsset  30655  dfon3  30658  brbigcup  30664  brapply  30704  brcup  30705  brcap  30706  dfint3  30718
  Copyright terms: Public domain W3C validator