Theorem epelc 4758

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 4757	. 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 187   e. wcel 1867   _Vcvv 3078   class class class wbr 4417   _E cep 4754

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pr 4652

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-rab 2782  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-br 4418  df-opab 4476  df-eprel 4756

This theorem is referenced by:  epel  4759  epini  5209  smoiso  7080  smoiso2  7087  ecid  7427  ordiso2  8021  oismo  8046  cantnflt  8167  cantnfp1lem3  8175  oemapso  8177  cantnflem1b  8181  cantnflem1  8184  cantnf  8188  wemapwe  8192  cnfcomlem  8194  cnfcom  8195  cnfcom3lem  8198  leweon  8432  r0weon  8433  alephiso  8518  fin23lem27  8747  fpwwe2lem9  9052  ex-eprel  25754  dftr6  30203  coep  30204  coepr  30205  brsset  30467  brtxpsd  30472  brcart  30510  dfrecs2  30528  dfrdg4  30529  cnambfre  31722  wepwsolem  35639  dnwech  35645