Theorem epelc 4746

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 4745	. 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 188   e. wcel 1886   _Vcvv 3044   class class class wbr 4401   _E cep 4742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-rab 2745  df-v 3046  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-br 4402  df-opab 4461  df-eprel 4744

This theorem is referenced by:  epel  4747  epini  5197  smoiso  7078  smoiso2  7085  ecid  7425  ordiso2  8027  oismo  8052  cantnflt  8174  cantnfp1lem3  8182  oemapso  8184  cantnflem1b  8188  cantnflem1  8191  cantnf  8195  wemapwe  8199  cnfcomlem  8201  cnfcom  8202  cnfcom3lem  8205  leweon  8439  r0weon  8440  alephiso  8526  fin23lem27  8755  fpwwe2lem9  9060  ex-eprel  25876  dftr6  30383  coep  30384  coepr  30385  brsset  30649  brtxpsd  30654  brcart  30692  dfrecs2  30710  dfrdg4  30711  cnambfre  31982  wepwsolem  35894  dnwech  35900