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

Theorem abid2 2882
Description: A simplification of class abstraction. Commuted form of abid1 2881. See comments there. (Contributed by NM, 26-Dec-1993.)
Assertion
Ref Expression
abid2 {𝑥𝑥𝐴} = 𝐴
Distinct variable group:   𝑥,𝐴

Proof of Theorem abid2
StepHypRef Expression
1 abid1 2881 . 2 𝐴 = {𝑥𝑥𝐴}
21eqcomi 2749 1 {𝑥𝑥𝐴} = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537  wcel 2108  {cab 2717
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819
This theorem is referenced by:  csbid  3934  csbconstg  3940  csbie  3957  abss  4086  ssab  4087  abssi  4093  notab  4333  dfrab3  4338  notrab  4341  eusn  4755  uniintsn  5009  iunidOLD  5084  axrep6g  5311  csbexg  5328  imai  6105  dffv4  6919  orduniss2  7871  dfixp  8959  euen1b  9094  modom2  9310  pwfir  9385  infmap2  10288  cshwsexaOLD  14875  ustfn  24233  ustn0  24252  lrrecse  27995  lrrecpred  27997  fpwrelmap  32749  eulerpartlemgvv  34343  ballotlem2  34455  dffv5  35890  ptrest  37581  cnambfre  37630  cnvepresex  38292  pmapglb  39729  polval2N  39865  rngunsnply  43132  iocinico  43175
  Copyright terms: Public domain W3C validator