Theorem epelc 4987

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

Syntax hints:   ↔ wb 196   ∈ wcel 1987  Vcvv 3186   class class class wbr 4613   E cep 4983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pr 4867

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-br 4614  df-opab 4674  df-eprel 4985

This theorem is referenced by:  epel  4988  epini  5454  smoiso  7404  smoiso2  7411  ecid  7757  ordiso2  8364  oismo  8389  cantnflt  8513  cantnfp1lem3  8521  oemapso  8523  cantnflem1b  8527  cantnflem1  8530  cantnf  8534  wemapwe  8538  cnfcomlem  8540  cnfcom  8541  cnfcom3lem  8544  leweon  8778  r0weon  8779  alephiso  8865  fin23lem27  9094  fpwwe2lem9  9404  ex-eprel  27144  dftr6  31345  coep  31346  coepr  31347  brsset  31635  brtxpsd  31640  brcart  31678  dfrecs2  31696  dfrdg4  31697  cnambfre  33087  wepwsolem  37089  dnwech  37095