Theorem epeli 5526

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

Syntax hints:   ↔ wb 206   ∈ wcel 2113  Vcvv 3440   class class class wbr 5098   E cep 5523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-eprel 5524

This theorem is referenced by:  epel  5527  0sn0ep  5528  smoiso  8294  smoiso2  8301  ecid  8717  ordiso2  9420  cantnflt  9581  cantnfp1lem3  9589  oemapso  9591  cantnflem1b  9595  cantnflem1  9598  cantnf  9602  wemapwe  9606  cnfcomlem  9608  cnfcom  9609  cnfcom3lem  9612  leweon  9921  r0weon  9922  alephiso  10008  fin23lem27  10238  fpwwe2lem8  10549  oniso  28267  ex-eprel  30508  cardpred  35248  satefvfmla0  35612  satefvfmla1  35619  dftr6  35945  coep  35946  coepr  35947  brsset  36081  brtxpsd  36086  brcart  36124  dfrecs2  36144  dfrdg4  36145  cnambfre  37865  wepwsolem  43280  dnwech  43286  rankrelp  45197