Theorem epeli 5257

Description: The membership relation and the membership predicate agree when the "containing" class is a set. Inference associated with epelg 5256. (Contributed by Scott Fenton, 11-Apr-2012.)

Hypothesis

Ref	Expression
epeli.1	⊢ 𝐵 ∈ V

Assertion

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

Proof of Theorem epeli

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

Syntax hints:   ↔ wb 198   ∈ wcel 2166  Vcvv 3414   class class class wbr 4873   E cep 5254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pr 5127

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-br 4874  df-opab 4936  df-eprel 5255

This theorem is referenced by:  epel  5258  0sn0ep  5259  epini  5736  smoiso  7725  smoiso2  7732  ecid  8077  ordiso2  8689  cantnflt  8846  cantnfp1lem3  8854  oemapso  8856  cantnflem1b  8860  cantnflem1  8863  cantnf  8867  wemapwe  8871  cnfcomlem  8873  cnfcom  8874  cnfcom3lem  8877  leweon  9147  r0weon  9148  alephiso  9234  fin23lem27  9465  fpwwe2lem9  9775  ex-eprel  27848  dftr6  32182  coep  32183  coepr  32184  brsset  32535  brtxpsd  32540  brcart  32578  dfrecs2  32596  dfrdg4  32597  cnambfre  34001  wepwsolem  38455  dnwech  38461