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

Theorem abid2 2401
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 229 . . 3  |-  ( x  e.  A  <->  x  e.  A )
21abbi2i 2395 . 2  |-  A  =  { x  |  x  e.  A }
32eqcomi 2288 1  |-  { x  |  x  e.  A }  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1624    e. wcel 1685   {cab 2270
This theorem is referenced by:  csbid  3089  csbexg  3092  abss  3243  ssab  3244  abssi  3249  notab  3439  inrab2  3442  dfrab2  3444  dfrab3  3445  notrab  3446  eusn  3704  uniintsn  3900  iunid  3958  orduniss2  4623  imai  5026  dffv3  6280  riotav  6304  cbvriota  6310  riotaund  6336  dfixp  6814  euen1b  6927  modom2  7059  infmap2  7839  ballotlem2  23040  dffv4  23870  mapex2  24539  prismorcsetlemb  25312  aomclem4  26553  rngunsnply  26777  compneOLD  27042  pmapglb  29226  polval2N  29362
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280
  Copyright terms: Public domain W3C validator