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

Theorem epel 5462
Description: The membership relation and the membership predicate agree when the "containing" class is a setvar. (Contributed by NM, 13-Aug-1995.) Replace the first setvar variable with a class variable. (Revised by BJ, 13-Sep-2022.)
Assertion
Ref Expression
epel (𝐴 E 𝑥𝐴𝑥)

Proof of Theorem epel
StepHypRef Expression
1 vex 3495 . 2 𝑥 ∈ V
21epeli 5461 1 (𝐴 E 𝑥𝐴𝑥)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wcel 2105   class class class wbr 5057   E cep 5457
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058  df-opab 5120  df-eprel 5458
This theorem is referenced by:  epse  5531  dfepfr  5533  epfrc  5534  wecmpep  5540  wetrep  5541  dmep  5786  domepOLD  5787  rnep  5790  epweon  7486  smoiso  7988  smoiso2  7995  ordunifi  8756  ordiso2  8967  ordtypelem8  8977  oismo  8992  wofib  8997  dford2  9071  noinfep  9111  oemapso  9133  wemapwe  9148  alephiso  9512  cflim2  9673  fin23lem27  9738  om2uzisoi  13310  bnj219  31902  efrunt  32836  dftr6  32883  dffr5  32886  elpotr  32923  dfon2lem9  32933  dfon2  32934  brsset  33247  dfon3  33250  brbigcup  33256  brapply  33296  brcup  33297  brcap  33298  dfint3  33310  dfssr2  35619
  Copyright terms: Public domain W3C validator