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

Theorem epel 5182
Description: The epsilon relation and the membership relation are the same. (Contributed by NM, 13-Aug-1995.)
Assertion
Ref Expression
epel (𝑥 E 𝑦𝑥𝑦)

Proof of Theorem epel
StepHypRef Expression
1 vex 3343 . 2 𝑦 ∈ V
21epelc 5181 1 (𝑥 E 𝑦𝑥𝑦)
Colors of variables: wff setvar class
Syntax hints:  wb 196   class class class wbr 4804   E cep 5178
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-opab 4865  df-eprel 5179
This theorem is referenced by:  epse  5249  dfepfr  5251  epfrc  5252  wecmpep  5258  wetrep  5259  ordon  7148  smoiso  7629  smoiso2  7636  ordunifi  8377  ordiso2  8587  ordtypelem8  8597  wofib  8617  dford2  8692  noinfep  8732  oemapso  8754  wemapwe  8769  alephiso  9131  cflim2  9297  fin23lem27  9362  om2uzisoi  12967  bnj219  31129  efrunt  31918  dftr6  31968  dffr5  31971  elpotr  32012  dfon2lem9  32022  dfon2  32023  domep  32024  brsset  32323  dfon3  32326  brbigcup  32332  brapply  32372  brcup  32373  brcap  32374  dfint3  32386  dfssr2  34590
  Copyright terms: Public domain W3C validator