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

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

Proof of Theorem abid2
StepHypRef Expression
1 abid1 2773 . 2 𝐴 = {𝑥𝑥𝐴}
21eqcomi 2660 1 {𝑥𝑥𝐴} = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  wcel 2030  {cab 2637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647
This theorem is referenced by:  csbid  3574  abss  3704  ssab  3705  abssi  3710  notab  3930  dfrab3  3935  notrab  3937  eusn  4297  uniintsn  4546  iunid  4607  csbexg  4825  imai  5513  dffv4  6226  orduniss2  7075  dfixp  7952  euen1b  8068  modom2  8203  infmap2  9078  cshwsexa  13616  ustfn  22052  ustn0  22071  fpwrelmap  29636  eulerpartlemgvv  30566  ballotlem2  30678  dffv5  32156  ptrest  33538  cnambfre  33588  cnvepresex  34245  pmapglb  35374  polval2N  35510  rngunsnply  38060  iocinico  38114
  Copyright terms: Public domain W3C validator