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

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

Proof of Theorem abid2
StepHypRef Expression
1 abid1 2869 . 2 𝐴 = {𝑥𝑥𝐴}
21eqcomi 2740 1 {𝑥𝑥𝐴} = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  wcel 2105  {cab 2708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809
This theorem is referenced by:  csbid  3906  csbconstg  3912  csbie  3929  abss  4057  ssab  4058  abssi  4067  notab  4304  dfrab3  4309  notrab  4311  eusn  4734  uniintsn  4991  iunidOLD  5064  axrep6g  5293  csbexg  5310  imai  6073  dffv4  6888  orduniss2  7825  dfixp  8897  euen1b  9031  pwfir  9180  modom2  9249  infmap2  10217  cshwsexaOLD  14780  ustfn  23927  ustn0  23946  lrrecse  27665  lrrecpred  27667  fpwrelmap  32226  eulerpartlemgvv  33674  ballotlem2  33786  dffv5  35201  ptrest  36791  cnambfre  36840  cnvepresex  37507  pmapglb  38945  polval2N  39081  rngunsnply  42218  iocinico  42264
  Copyright terms: Public domain W3C validator