Theorem epeli 5525

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3438   class class class wbr 5095   E cep 5522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-eprel 5523

This theorem is referenced by:  epel  5526  0sn0ep  5527  smoiso  8292  smoiso2  8299  ecid  8714  ordiso2  9426  cantnflt  9587  cantnfp1lem3  9595  oemapso  9597  cantnflem1b  9601  cantnflem1  9604  cantnf  9608  wemapwe  9612  cnfcomlem  9614  cnfcom  9615  cnfcom3lem  9618  leweon  9924  r0weon  9925  alephiso  10011  fin23lem27  10241  fpwwe2lem8  10551  onsiso  28192  ex-eprel  30395  cardpred  35056  satefvfmla0  35390  satefvfmla1  35397  dftr6  35723  coep  35724  coepr  35725  brsset  35862  brtxpsd  35867  brcart  35905  dfrecs2  35923  dfrdg4  35924  cnambfre  37647  wepwsolem  43015  dnwech  43021  rankrelp  44934