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

Theorem abid2 2375
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 2369 . 2  |-  A  =  { x  |  x  e.  A }
32eqcomi 2262 1  |-  { x  |  x  e.  A }  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1619    e. wcel 1621   {cab 2244
This theorem is referenced by:  csbid  3063  csbexg  3066  abss  3217  ssab  3218  abssi  3223  notab  3413  inrab2  3416  dfrab2  3418  dfrab3  3419  notrab  3420  eusn  3677  uniintsn  3873  iunid  3931  orduniss2  4596  imai  5015  dffv3  6253  riotav  6277  cbvriota  6283  riotaund  6309  dfixp  6787  euen1b  6900  modom2  7032  infmap2  7812  ballotlem2  23008  dffv4  23838  mapex2  24507  prismorcsetlemb  25280  aomclem4  26521  rngunsnply  26745  compneOLD  27011  pmapglb  29126  polval2N  29262
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254
  Copyright terms: Public domain W3C validator