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

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

Proof of Theorem abid2
StepHypRef Expression
1 abid1 2893 . 2 𝐴 = {𝑥𝑥𝐴}
21eqcomi 2780 1 {𝑥𝑥𝐴} = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1631  wcel 2145  {cab 2757
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767
This theorem is referenced by:  csbid  3691  abss  3821  ssab  3822  abssi  3827  notab  4046  dfrab3  4051  notrab  4053  eusn  4402  uniintsn  4649  iunid  4710  csbexg  4927  imai  5620  dffv4  6330  orduniss2  7181  dfixp  8065  euen1b  8181  modom2  8319  infmap2  9243  cshwsexa  13780  ustfn  22226  ustn0  22245  fpwrelmap  29849  eulerpartlemgvv  30779  ballotlem2  30891  dffv5  32369  ptrest  33742  cnambfre  33791  cnvepresex  34448  pmapglb  35579  polval2N  35715  rngunsnply  38270  iocinico  38324
  Copyright terms: Public domain W3C validator