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

Theorem epel 5437
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 3447 . 2 𝑥 ∈ V
21epeli 5436 1 (𝐴 E 𝑥𝐴𝑥)
Colors of variables: wff setvar class
Syntax hints:  wb 209  wcel 2112   class class class wbr 5033   E cep 5432
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298
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 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034  df-opab 5096  df-eprel 5433
This theorem is referenced by:  epse  5506  dfepfr  5508  epfrc  5509  wecmpep  5515  wetrep  5516  dmep  5761  domepOLD  5762  rnep  5765  epweon  7481  smoiso  7986  smoiso2  7993  ordunifi  8756  ordiso2  8967  ordtypelem8  8977  oismo  8992  wofib  8997  dford2  9071  noinfep  9111  oemapso  9133  wemapwe  9148  alephiso  9513  cflim2  9678  fin23lem27  9743  om2uzisoi  13321  bnj219  32111  efrunt  33047  dftr6  33094  dffr5  33097  elpotr  33134  dfon2lem9  33144  dfon2  33145  brsset  33458  dfon3  33461  brbigcup  33467  brapply  33507  brcup  33508  brcap  33509  dfint3  33521  dfssr2  35892
  Copyright terms: Public domain W3C validator