MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  epeli Structured version   Visualization version   GIF version

Theorem epeli 5441
Description: The membership relation and the membership predicate agree when the "containing" class is a set. Inference associated with epelg 5439. (Contributed by Scott Fenton, 11-Apr-2012.)
Hypothesis
Ref Expression
epeli.1 𝐵 ∈ V
Assertion
Ref Expression
epeli (𝐴 E 𝐵𝐴𝐵)

Proof of Theorem epeli
StepHypRef Expression
1 epeli.1 . 2 𝐵 ∈ V
2 epelg 5439 . 2 (𝐵 ∈ V → (𝐴 E 𝐵𝐴𝐵))
31, 2ax-mp 5 1 (𝐴 E 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 209  wcel 2115  Vcvv 3471   class class class wbr 5039   E cep 5437
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 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pr 5303
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-rab 3135  df-v 3473  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-sn 4541  df-pr 4543  df-op 4547  df-br 5040  df-opab 5102  df-eprel 5438
This theorem is referenced by:  epel  5442  0sn0ep  5443  epini  5932  smoiso  7974  smoiso2  7981  ecid  8337  ordiso2  8955  cantnflt  9111  cantnfp1lem3  9119  oemapso  9121  cantnflem1b  9125  cantnflem1  9128  cantnf  9132  wemapwe  9136  cnfcomlem  9138  cnfcom  9139  cnfcom3lem  9142  leweon  9414  r0weon  9415  alephiso  9501  fin23lem27  9727  fpwwe2lem9  10037  ex-eprel  28197  satefvfmla0  32673  satefvfmla1  32680  dftr6  32994  coep  32995  coepr  32996  brsset  33358  brtxpsd  33363  brcart  33401  dfrecs2  33419  dfrdg4  33420  cnambfre  34987  wepwsolem  39793  dnwech  39799
  Copyright terms: Public domain W3C validator