Theorem epelc 5179

Description: The epsilon relationship and the membership relation are the same. (Contributed by Scott Fenton, 11-Apr-2012.)

Hypothesis

Ref	Expression
epelc.1	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
epelc	⊢ (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)

Proof of Theorem epelc

Step	Hyp	Ref	Expression
1		epelc.1	. 2 ⊢ 𝐵 ∈ V
2		epelg 5178	. 2 ⊢ (𝐵 ∈ V → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)

Syntax hints:   ↔ wb 196   ∈ wcel 2137  Vcvv 3338   class class class wbr 4802   E cep 5176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931  ax-nul 4939  ax-pr 5053

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-rab 3057  df-v 3340  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-if 4229  df-sn 4320  df-pr 4322  df-op 4326  df-br 4803  df-opab 4863  df-eprel 5177

This theorem is referenced by:  epel  5180  0sn0ep  5181  epini  5651  smoiso  7626  smoiso2  7633  ecid  7977  ordiso2  8583  oismo  8608  cantnflt  8740  cantnfp1lem3  8748  oemapso  8750  cantnflem1b  8754  cantnflem1  8757  cantnf  8761  wemapwe  8765  cnfcomlem  8767  cnfcom  8768  cnfcom3lem  8771  leweon  9022  r0weon  9023  alephiso  9109  fin23lem27  9340  fpwwe2lem9  9650  ex-eprel  27599  dftr6  31945  coep  31946  coepr  31947  brsset  32300  brtxpsd  32305  brcart  32343  dfrecs2  32361  dfrdg4  32362  cnambfre  33769  wepwsolem  38112  dnwech  38118