Theorem epeli 5543

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3450   class class class wbr 5110   E cep 5540

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-eprel 5541

This theorem is referenced by:  epel  5544  0sn0ep  5545  smoiso  8334  smoiso2  8341  ecid  8756  ordiso2  9475  cantnflt  9632  cantnfp1lem3  9640  oemapso  9642  cantnflem1b  9646  cantnflem1  9649  cantnf  9653  wemapwe  9657  cnfcomlem  9659  cnfcom  9660  cnfcom3lem  9663  leweon  9971  r0weon  9972  alephiso  10058  fin23lem27  10288  fpwwe2lem8  10598  onsiso  28176  ex-eprel  30369  cardpred  35087  satefvfmla0  35412  satefvfmla1  35419  dftr6  35745  coep  35746  coepr  35747  brsset  35884  brtxpsd  35889  brcart  35927  dfrecs2  35945  dfrdg4  35946  cnambfre  37669  wepwsolem  43038  dnwech  43044  rankrelp  44957