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

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

Proof of Theorem abid2
StepHypRef Expression
1 abid1 2626 . 2 𝐴 = {𝑥𝑥𝐴}
21eqcomi 2514 1 {𝑥𝑥𝐴} = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1468  wcel 1937  {cab 2491
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485
This theorem depends on definitions:  df-bi 192  df-an 380  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-clab 2492  df-cleq 2498  df-clel 2501
This theorem is referenced by:  csbid  3393  abss  3520  ssab  3521  abssi  3526  notab  3739  dfrab3  3744  notrab  3746  eusn  4076  uniintsn  4301  iunid  4362  csbexg  4570  imai  5230  dffv4  5924  orduniss2  6737  dfixp  7607  euen1b  7724  modom2  7858  infmap2  8733  cshwsexa  13059  ustfn  21374  ustn0  21393  fpwrelmap  28474  eulerpartlemgvv  29363  ballotlem2  29475  dffv5  30842  ptrest  32177  cnambfre  32227  pmapglb  33575  polval2N  33711  rngunsnply  36279  iocinico  36336
  Copyright terms: Public domain W3C validator