Theorem epeli 5518

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

Syntax hints:   ↔ wb 206   ∈ wcel 2111  Vcvv 3436   class class class wbr 5091   E cep 5515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-br 5092  df-opab 5154  df-eprel 5516

This theorem is referenced by:  epel  5519  0sn0ep  5520  smoiso  8282  smoiso2  8289  ecid  8704  ordiso2  9401  cantnflt  9562  cantnfp1lem3  9570  oemapso  9572  cantnflem1b  9576  cantnflem1  9579  cantnf  9583  wemapwe  9587  cnfcomlem  9589  cnfcom  9590  cnfcom3lem  9593  leweon  9899  r0weon  9900  alephiso  9986  fin23lem27  10216  fpwwe2lem8  10526  onsiso  28203  ex-eprel  30408  cardpred  35098  satefvfmla0  35450  satefvfmla1  35457  dftr6  35783  coep  35784  coepr  35785  brsset  35922  brtxpsd  35927  brcart  35965  dfrecs2  35983  dfrdg4  35984  cnambfre  37707  wepwsolem  43074  dnwech  43080  rankrelp  44992