Theorem epeli 5540

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3447   class class class wbr 5107   E cep 5537

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 5251  ax-nul 5261  ax-pr 5387

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-eprel 5538

This theorem is referenced by:  epel  5541  0sn0ep  5542  smoiso  8331  smoiso2  8338  ecid  8753  ordiso2  9468  cantnflt  9625  cantnfp1lem3  9633  oemapso  9635  cantnflem1b  9639  cantnflem1  9642  cantnf  9646  wemapwe  9650  cnfcomlem  9652  cnfcom  9653  cnfcom3lem  9656  leweon  9964  r0weon  9965  alephiso  10051  fin23lem27  10281  fpwwe2lem8  10591  onsiso  28169  ex-eprel  30362  cardpred  35080  satefvfmla0  35405  satefvfmla1  35412  dftr6  35738  coep  35739  coepr  35740  brsset  35877  brtxpsd  35882  brcart  35920  dfrecs2  35938  dfrdg4  35939  cnambfre  37662  wepwsolem  43031  dnwech  43037  rankrelp  44950