Theorem epeli 5586

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

Syntax hints:   ↔ wb 206   ∈ wcel 2108  Vcvv 3480   class class class wbr 5143   E cep 5583

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-eprel 5584

This theorem is referenced by:  epel  5587  0sn0ep  5588  smoiso  8402  smoiso2  8409  ecid  8822  ordiso2  9555  cantnflt  9712  cantnfp1lem3  9720  oemapso  9722  cantnflem1b  9726  cantnflem1  9729  cantnf  9733  wemapwe  9737  cnfcomlem  9739  cnfcom  9740  cnfcom3lem  9743  leweon  10051  r0weon  10052  alephiso  10138  fin23lem27  10368  fpwwe2lem8  10678  ex-eprel  30452  cardpred  35104  satefvfmla0  35423  satefvfmla1  35430  dftr6  35751  coep  35752  coepr  35753  brsset  35890  brtxpsd  35895  brcart  35933  dfrecs2  35951  dfrdg4  35952  cnambfre  37675  wepwsolem  43054  dnwech  43060  rankrelp  44977