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

Theorem abid2 2413
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 227 . . 3  |-  ( x  e.  A  <->  x  e.  A )
21abbi2i 2407 . 2  |-  A  =  { x  |  x  e.  A }
32eqcomi 2300 1  |-  { x  |  x  e.  A }  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1632    e. wcel 1696   {cab 2282
This theorem is referenced by:  csbid  3101  csbexg  3104  abss  3255  ssab  3256  abssi  3261  notab  3451  inrab2  3454  dfrab2  3456  dfrab3  3457  notrab  3458  eusn  3716  uniintsn  3915  iunid  3973  orduniss2  4640  imai  5043  dffv4  5538  riotav  6325  cbvriota  6331  riotaund  6357  dfixp  6835  euen1b  6948  modom2  7080  infmap2  7860  ballotlem2  23063  dffv5  24534  mapex2  25243  prismorcsetlemb  26016  aomclem4  27257  rngunsnply  27481  compneOLD  27746  pmapglb  30581  polval2N  30717
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292
  Copyright terms: Public domain W3C validator