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

Theorem abid2 2607
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 236 . . 3  |-  ( x  e.  A  <->  x  e.  A )
21abbi2i 2600 . 2  |-  A  =  { x  |  x  e.  A }
32eqcomi 2480 1  |-  { x  |  x  e.  A }  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379    e. wcel 1767   {cab 2452
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462
This theorem is referenced by:  csbid  3443  abss  3569  ssab  3570  abssi  3575  notab  3768  inrab2  3771  dfrab3  3773  notrab  3775  eusn  4103  uniintsn  4319  iunid  4380  csbexg  4579  csbexgOLD  4581  imai  5348  dffv4  5862  orduniss2  6647  dfixp  7471  euen1b  7586  modom2  7721  infmap2  8597  cshwsexa  12754  ustfn  20455  ustn0  20474  fpwrelmap  27244  eulerpartlemgvv  27971  ballotlem2  28083  dffv5  29167  ptrest  29641  cnambfre  29656  aomclem4  30623  rngunsnply  30743  iocinico  30800  riotaclbgBAD  33766  riotaclbBAD  33767  pmapglb  34575  polval2N  34711
  Copyright terms: Public domain W3C validator