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

Theorem abid2 2400
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 2394 . 2  |-  A  =  { x  |  x  e.  A }
32eqcomi 2287 1  |-  { x  |  x  e.  A }  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1623    e. wcel 1684   {cab 2269
This theorem is referenced by:  csbid  3088  csbexg  3091  abss  3242  ssab  3243  abssi  3248  notab  3438  inrab2  3441  dfrab2  3443  dfrab3  3444  notrab  3445  eusn  3703  uniintsn  3899  iunid  3957  orduniss2  4624  imai  5027  dffv4  5522  riotav  6309  cbvriota  6315  riotaund  6341  dfixp  6819  euen1b  6932  modom2  7064  infmap2  7844  ballotlem2  23047  dffv5  24463  mapex2  25140  prismorcsetlemb  25913  aomclem4  27154  rngunsnply  27378  compneOLD  27643  pmapglb  29959  polval2N  30095
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279
  Copyright terms: Public domain W3C validator