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

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

Proof of Theorem abid2
StepHypRef Expression
1 abid1 2925 . 2 𝐴 = {𝑥𝑥𝐴}
21eqcomi 2804 1 {𝑥𝑥𝐴} = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1522  wcel 2081  {cab 2775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-ext 2769
This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1525  df-ex 1762  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863
This theorem is referenced by:  csbid  3823  abss  3961  ssab  3962  abssi  3967  notab  4193  dfrab3  4198  notrab  4200  eusn  4573  uniintsn  4819  iunid  4883  csbexg  5105  imai  5818  dffv4  6535  orduniss2  7404  dfixp  8312  euen1b  8428  modom2  8566  infmap2  9486  cshwsexa  14022  ustfn  22493  ustn0  22512  fpwrelmap  30157  eulerpartlemgvv  31251  ballotlem2  31363  dffv5  32994  ptrest  34422  cnambfre  34471  cnvepresex  35123  pmapglb  36437  polval2N  36573  rngunsnply  39258  iocinico  39303
  Copyright terms: Public domain W3C validator