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

Theorem abid2 2553
Description: A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35. (Contributed by NM, 26-Dec-1993.)
Assertion
Ref Expression
abid2  |-  { x  |  x  e.  A }  =  A
Distinct variable group:    x, A

Proof of Theorem abid2
StepHypRef Expression
1 biid 228 . . 3  |-  ( x  e.  A  <->  x  e.  A )
21abbi2i 2547 . 2  |-  A  =  { x  |  x  e.  A }
32eqcomi 2440 1  |-  { x  |  x  e.  A }  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1652    e. wcel 1725   {cab 2422
This theorem is referenced by:  csbid  3258  csbexg  3261  abss  3412  ssab  3413  abssi  3418  notab  3611  inrab2  3614  dfrab2  3616  dfrab3  3617  notrab  3618  eusn  3880  uniintsn  4087  iunid  4146  orduniss2  4813  imai  5218  dffv4  5725  riotav  6554  cbvriota  6560  riotaund  6586  dfixp  7065  euen1b  7178  modom2  7310  infmap2  8098  ustfn  18231  ustn0  18250  ballotlem2  24746  dffv5  25769  cnambfre  26255  aomclem4  27132  rngunsnply  27355  cshwsexa  28291  pmapglb  30567  polval2N  30703
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432
  Copyright terms: Public domain W3C validator