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

Theorem abid2 2594
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 2587 . 2  |-  A  =  { x  |  x  e.  A }
32eqcomi 2467 1  |-  { x  |  x  e.  A }  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398    e. wcel 1823   {cab 2439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449
This theorem is referenced by:  csbid  3428  abss  3555  ssab  3556  abssi  3561  notab  3765  inrab2  3768  dfrab3  3770  notrab  3772  eusn  4092  uniintsn  4309  iunid  4370  csbexg  4571  imai  5337  dffv4  5845  orduniss2  6641  dfixp  7464  euen1b  7579  modom2  7714  infmap2  8589  cshwsexa  12786  ustfn  20873  ustn0  20892  fpwrelmap  27790  eulerpartlemgvv  28582  ballotlem2  28694  dffv5  29805  ptrest  30291  cnambfre  30306  aomclem4  31245  rngunsnply  31366  iocinico  31423  riotaclbgBAD  35101  pmapglb  35910  polval2N  36046
  Copyright terms: Public domain W3C validator