Theorem epeli 5534

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  Vcvv 3442   class class class wbr 5100   E cep 5531

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 2709  ax-sep 5243  ax-pr 5379

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 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-eprel 5532

This theorem is referenced by:  epel  5535  0sn0ep  5536  smoiso  8304  smoiso2  8311  ecid  8729  ordiso2  9432  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  28279  ex-eprel  30520  cardpred  35267  satefvfmla0  35631  satefvfmla1  35638  dftr6  35964  coep  35965  coepr  35966  brsset  36100  brtxpsd  36105  brcart  36143  dfrecs2  36163  dfrdg4  36164  cnambfre  37913  wepwsolem  43393  dnwech  43399  rankrelp  45310