Theorem epelc 5060

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 5059	. 2 ⊢ (𝐵 ∈ V → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)

Syntax hints:   ↔ wb 196   ∈ wcel 2030  Vcvv 3231   class class class wbr 4685   E cep 5057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-eprel 5058

This theorem is referenced by:  epel  5061  epini  5530  smoiso  7504  smoiso2  7511  ecid  7855  ordiso2  8461  oismo  8486  cantnflt  8607  cantnfp1lem3  8615  oemapso  8617  cantnflem1b  8621  cantnflem1  8624  cantnf  8628  wemapwe  8632  cnfcomlem  8634  cnfcom  8635  cnfcom3lem  8638  leweon  8872  r0weon  8873  alephiso  8959  fin23lem27  9188  fpwwe2lem9  9498  ex-eprel  27420  dftr6  31766  coep  31767  coepr  31768  brsset  32121  brtxpsd  32126  brcart  32164  dfrecs2  32182  dfrdg4  32183  cnambfre  33588  wepwsolem  37929  dnwech  37935