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

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

Proof of Theorem abid2
StepHypRef Expression
1 abid1 2894 . 2 𝐴 = {𝑥𝑥𝐴}
21eqcomi 2768 1 {𝑥𝑥𝐴} = 𝐴
 Colors of variables: wff setvar class Syntax hints:   = wceq 1539   ∈ wcel 2112  {cab 2736 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730 This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831 This theorem is referenced by:  csbid  3819  abss  3966  ssab  3967  abssi  3975  notab  4208  dfrab3  4213  notrab  4215  eusn  4621  uniintsn  4875  iunid  4947  csbexg  5178  imai  5912  dffv4  6653  orduniss2  7545  dfixp  8479  euen1b  8597  modom2  8739  infmap2  9668  cshwsexa  14223  ustfn  22892  ustn0  22911  fpwrelmap  30582  eulerpartlemgvv  31852  ballotlem2  31964  lrrecse  33636  lrrecpred  33638  addsid1  33665  dffv5  33765  ptrest  35326  cnambfre  35375  cnvepresex  36021  pmapglb  37336  polval2N  37472  rngunsnply  40480  iocinico  40525
 Copyright terms: Public domain W3C validator