Theorem epeli 5553

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2145  Vcvv 3451   class class class wbr 5103   E cep 5550

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-eprel 5551

This theorem is used by:  epel  5554  0sn0ep  5555  smoiso  8354  smoiso2  8361  ecid  8785  ordiso2  9493  cantnflt  9657  cantnfp1lem3  9665  oemapso  9667  cantnflem1b  9671  cantnflem1  9674  cantnf  9678  wemapwe  9682  cnfcomlem  9684  cnfcom  9685  cnfcom3lem  9688  leweon  10071  r0weon  10072  alephiso  10158  fin23lem27  10387  fpwwe2lem8  10704  oniso  28639  ex-eprel  31016  cardpred  35700  vonf1osev  35864  satefvfmla0  36152  satefvfmla1  36159  dftr6  36485  coep  36486  coepr  36487  brsset  36621  brtxpsd  36626  brcart  36664  dfrecs2  36684  dfrdg4  36685  cnambfre  38554  wepwsolem  44002  dnwech  44008  rankrelp  45902