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

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

Proof of Theorem abid2
StepHypRef Expression
1 abid1 2730 . 2 𝐴 = {𝑥𝑥𝐴}
21eqcomi 2618 1 {𝑥𝑥𝐴} = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wcel 1976  {cab 2595
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605
This theorem is referenced by:  csbid  3506  abss  3633  ssab  3634  abssi  3639  notab  3855  dfrab3  3860  notrab  3862  eusn  4208  uniintsn  4443  iunid  4505  csbexg  4715  imai  5384  dffv4  6085  orduniss2  6902  dfixp  7773  euen1b  7890  modom2  8024  infmap2  8900  cshwsexa  13367  ustfn  21757  ustn0  21776  fpwrelmap  28702  eulerpartlemgvv  29571  ballotlem2  29683  dffv5  31007  ptrest  32374  cnambfre  32424  pmapglb  33870  polval2N  34006  rngunsnply  36558  iocinico  36612
  Copyright terms: Public domain W3C validator