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

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

Proof of Theorem abid2
StepHypRef Expression
1 abid1 2635 . 2 𝐴 = {𝑥𝑥𝐴}
21eqcomi 2523 1 {𝑥𝑥𝐴} = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wcel 1938  {cab 2500
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494
This theorem depends on definitions:  df-bi 195  df-an 384  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510
This theorem is referenced by:  csbid  3411  abss  3538  ssab  3539  abssi  3544  notab  3759  dfrab3  3764  notrab  3766  eusn  4112  uniintsn  4347  iunid  4409  csbexg  4619  imai  5288  dffv4  5989  orduniss2  6806  dfixp  7676  euen1b  7793  modom2  7927  infmap2  8803  cshwsexa  13284  ustfn  21722  ustn0  21741  fpwrelmap  28688  eulerpartlemgvv  29576  ballotlem2  29688  dffv5  31040  ptrest  32472  cnambfre  32522  pmapglb  33968  polval2N  34104  rngunsnply  36663  iocinico  36717
  Copyright terms: Public domain W3C validator