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

Theorem abid2 2521
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 2515 . 2  |-  A  =  { x  |  x  e.  A }
32eqcomi 2408 1  |-  { x  |  x  e.  A }  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1649    e. wcel 1721   {cab 2390
This theorem is referenced by:  csbid  3218  csbexg  3221  abss  3372  ssab  3373  abssi  3378  notab  3571  inrab2  3574  dfrab2  3576  dfrab3  3577  notrab  3578  eusn  3840  uniintsn  4047  iunid  4106  orduniss2  4772  imai  5177  dffv4  5684  riotav  6513  cbvriota  6519  riotaund  6545  dfixp  7024  euen1b  7137  modom2  7269  infmap2  8054  ustfn  18184  ustn0  18203  ballotlem2  24699  dffv5  25677  cnambfre  26154  aomclem4  27022  rngunsnply  27246  pmapglb  30252  polval2N  30388
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400
  Copyright terms: Public domain W3C validator