Theorem epeli 5536

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  Vcvv 3442   class class class wbr 5100   E cep 5533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5245  ax-pr 5381

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-eprel 5534

This theorem is referenced by:  epel  5537  0sn0ep  5538  smoiso  8306  smoiso2  8313  ecid  8731  ordiso2  9434  cantnflt  9595  cantnfp1lem3  9603  oemapso  9605  cantnflem1b  9609  cantnflem1  9612  cantnf  9616  wemapwe  9620  cnfcomlem  9622  cnfcom  9623  cnfcom3lem  9626  leweon  9935  r0weon  9936  alephiso  10022  fin23lem27  10252  fpwwe2lem8  10563  oniso  28284  ex-eprel  30526  cardpred  35275  satefvfmla0  35640  satefvfmla1  35647  dftr6  35973  coep  35974  coepr  35975  brsset  36109  brtxpsd  36114  brcart  36152  dfrecs2  36172  dfrdg4  36173  cnambfre  37948  wepwsolem  43428  dnwech  43434  rankrelp  45345