Theorem epeli 5533

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  Vcvv 3429   class class class wbr 5085   E cep 5530

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 2708  ax-sep 5231  ax-pr 5375

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-eprel 5531

This theorem is referenced by:  epel  5534  0sn0ep  5535  smoiso  8302  smoiso2  8309  ecid  8727  ordiso2  9430  cantnflt  9593  cantnfp1lem3  9601  oemapso  9603  cantnflem1b  9607  cantnflem1  9610  cantnf  9614  wemapwe  9618  cnfcomlem  9620  cnfcom  9621  cnfcom3lem  9624  leweon  9933  r0weon  9934  alephiso  10020  fin23lem27  10250  fpwwe2lem8  10561  oniso  28263  ex-eprel  30503  cardpred  35235  satefvfmla0  35600  satefvfmla1  35607  dftr6  35933  coep  35934  coepr  35935  brsset  36069  brtxpsd  36074  brcart  36112  dfrecs2  36132  dfrdg4  36133  cnambfre  37989  wepwsolem  43470  dnwech  43476  rankrelp  45387