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

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

Proof of Theorem abid2
StepHypRef Expression
1 abid1 2731 . 2 𝐴 = {𝑥𝑥𝐴}
21eqcomi 2619 1 {𝑥𝑥𝐴} = 𝐴
 Colors of variables: wff setvar class Syntax hints:   = wceq 1475   ∈ wcel 1977  {cab 2596 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606 This theorem is referenced by:  csbid  3507  abss  3634  ssab  3635  abssi  3640  notab  3856  dfrab3  3861  notrab  3863  eusn  4209  uniintsn  4449  iunid  4511  csbexg  4720  imai  5397  dffv4  6100  orduniss2  6925  dfixp  7796  euen1b  7913  modom2  8047  infmap2  8923  cshwsexa  13421  ustfn  21815  ustn0  21834  fpwrelmap  28896  eulerpartlemgvv  29765  ballotlem2  29877  dffv5  31201  ptrest  32578  cnambfre  32628  pmapglb  34074  polval2N  34210  rngunsnply  36762  iocinico  36816
 Copyright terms: Public domain W3C validator