Theorem epeli 5527

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

Syntax hints:   ↔ wb 207   ∈ wcel 2119  Vcvv 3432   class class class wbr 5079   E cep 5524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-eprel 5525

This theorem is referenced by:  epel  5528  0sn0ep  5529  smoiso  8299  smoiso2  8306  ecid  8724  ordiso2  9427  cantnflt  9591  cantnfp1lem3  9599  oemapso  9601  cantnflem1b  9605  cantnflem1  9608  cantnf  9612  wemapwe  9616  cnfcomlem  9618  cnfcom  9619  cnfcom3lem  9622  leweon  9931  r0weon  9932  alephiso  10018  fin23lem27  10248  fpwwe2lem8  10559  oniso  28288  ex-eprel  30528  cardpred  35280  satefvfmla0  35653  satefvfmla1  35660  dftr6  35986  coep  35987  coepr  35988  brsset  36122  brtxpsd  36127  brcart  36165  dfrecs2  36185  dfrdg4  36186  cnambfre  38042  wepwsolem  43494  dnwech  43500  rankrelp  45411