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

Theorem epelc 4460
Description: The epsilon relationship and the membership relation are the same. (Contributed by Scott Fenton, 11-Apr-2012.)
Hypothesis
Ref Expression
epelc.1  |-  B  e. 
_V
Assertion
Ref Expression
epelc  |-  ( A  _E  B  <->  A  e.  B )

Proof of Theorem epelc
StepHypRef Expression
1 epelc.1 . 2  |-  B  e. 
_V
2 epelg 4459 . 2  |-  ( B  e.  _V  ->  ( A  _E  B  <->  A  e.  B ) )
31, 2ax-mp 8 1  |-  ( A  _E  B  <->  A  e.  B )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    e. wcel 1721   _Vcvv 2920   class class class wbr 4176    _E cep 4456
This theorem is referenced by:  epel  4461  epini  5197  smoiso  6587  smoiso2  6594  ecid  6932  ordiso2  7444  oismo  7469  cantnflt  7587  cantnfp1lem3  7596  oemapso  7598  cantnflem1b  7602  cantnflem1  7605  cantnf  7609  wemapwe  7614  cnfcomlem  7616  cnfcom  7617  cnfcom3lem  7620  leweon  7853  r0weon  7854  alephiso  7939  fin23lem27  8168  fpwwe2lem9  8473  ex-eprel  21698  dftr6  25325  coep  25326  coepr  25327  brsset  25647  brtxpsd  25652  brcart  25689  brcup  25696  brcap  25697  dfrdg4  25707  cnambfre  26158  wepwsolem  27010  dnwech  27017
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pr 4367
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-rab 2679  df-v 2922  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-op 3787  df-br 4177  df-opab 4231  df-eprel 4458
  Copyright terms: Public domain W3C validator