Theorem epeli 5552

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2144  Vcvv 3450   class class class wbr 5102   E cep 5549

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-eprel 5550

This theorem is used by:  epel  5553  0sn0ep  5554  smoiso  8373  smoiso2  8380  ecid  8804  ordiso2  9512  cantnflt  9676  cantnfp1lem3  9684  oemapso  9686  cantnflem1b  9690  cantnflem1  9693  cantnf  9697  wemapwe  9701  cnfcomlem  9703  cnfcom  9704  cnfcom3lem  9707  leweon  10093  r0weon  10094  alephiso  10180  fin23lem27  10409  fpwwe2lem8  10726  oniso  28662  ex-eprel  31039  onf1we  35771  cardpred  35773  werankwe  35791  werankwe2  35792  j00smo  35944  maxssj0  35945  vonf1osev  35959  satefvfmla0  36269  satefvfmla1  36276  dftr6  36608  coep  36609  coepr  36610  brsset  36743  brtxpsd  36748  brcart  36786  dfrecs2  36806  dfrdg4  36807  cnambfre  38679  wepwsolem  44142  dnwech  44148  rankrelp  46043