Theorem epelc 4639

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

Step	Hyp	Ref	Expression
1		epelc.1	. 2 |- B e. _V
2		epelg 4638	. 2 |- ( B e. _V -> ( A _E B <-> A e. B ) )
3	1, 2	ax-mp 5	1 |- ( A _E B <-> A e. B )

Syntax hints:   <-> wb 184   e. wcel 1756   _Vcvv 2977   class class class wbr 4297   _E cep 4635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-nul 4426  ax-pr 4536

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-rab 2729  df-v 2979  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-op 3889  df-br 4298  df-opab 4356  df-eprel 4637

This theorem is referenced by:  epel  4640  epini  5204  smoiso  6828  smoiso2  6835  ecid  7170  ordiso2  7734  oismo  7759  cantnflt  7885  cantnfp1lem3  7893  oemapso  7895  cantnflem1b  7899  cantnflem1  7902  cantnf  7906  cantnfltOLD  7915  cantnfp1lem3OLD  7919  cantnflem1bOLD  7922  cantnflem1OLD  7925  cantnfOLD  7928  wemapwe  7933  wemapweOLD  7934  cnfcomlem  7937  cnfcom  7938  cnfcom3lem  7941  cnfcomlemOLD  7945  cnfcomOLD  7946  cnfcom3lemOLD  7949  leweon  8183  r0weon  8184  alephiso  8273  fin23lem27  8502  fpwwe2lem9  8810  ex-eprel  23645  dftr6  27565  coep  27566  coepr  27567  brsset  27925  brtxpsd  27930  brcart  27968  dfrdg4  27986  cnambfre  28445  wepwsolem  29399  dnwech  29406