Theorem epeli 5488

Description: The membership relation and the membership predicate agree when the "containing" class is a set. Inference associated with epelg 5487. (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 5487	. 2 ⊢ (𝐵 ∈ V → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)

Syntax hints:   ↔ wb 205   ∈ wcel 2108  Vcvv 3422   class class class wbr 5070   E cep 5485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-eprel 5486

This theorem is referenced by:  epel  5489  0sn0ep  5490  smoiso  8164  smoiso2  8171  ecid  8529  ordiso2  9204  cantnflt  9360  cantnfp1lem3  9368  oemapso  9370  cantnflem1b  9374  cantnflem1  9377  cantnf  9381  wemapwe  9385  cnfcomlem  9387  cnfcom  9388  cnfcom3lem  9391  leweon  9698  r0weon  9699  alephiso  9785  fin23lem27  10015  fpwwe2lem8  10325  ex-eprel  28698  cardpred  32962  satefvfmla0  33280  satefvfmla1  33287  dftr6  33624  coep  33625  coepr  33626  brsset  34118  brtxpsd  34123  brcart  34161  dfrecs2  34179  dfrdg4  34180  cnambfre  35752  wepwsolem  40783  dnwech  40789