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

Theorem rabid 2884
Description: An "identity" law of concretion for restricted abstraction. Special case of Definition 2.1 of [Quine] p. 16. (Contributed by NM, 9-Oct-2003.)
Assertion
Ref Expression
rabid  |-  ( x  e.  { x  e.  A  |  ph }  <->  ( x  e.  A  /\  ph ) )

Proof of Theorem rabid
StepHypRef Expression
1 df-rab 2714 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
21abeq2i 2543 1  |-  ( x  e.  { x  e.  A  |  ph }  <->  ( x  e.  A  /\  ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359    e. wcel 1725   {crab 2709
This theorem is referenced by:  rabeq2i  2953  reusv2lem4  4727  reusv2  4729  rabxfrd  4744  tfis  4834  riotaxfrd  6581  rankr1ai  7724  cfval2  8140  cflim3  8142  cflim2  8143  cfss  8145  cfslb  8146  cofsmo  8149  nnwos  10544  ramval  13376  ramub1lem1  13394  neiptopnei  17196  hauseqlcld  17678  imasnopn  17722  imasncld  17723  imasncls  17724  ptcmplem4  18086  blval2  18605  metutopOLD  18612  psmetutop  18613  mbfinf  19557  itg2monolem1  19642  lhop1  19898  rabexgfGS  23987  rabss3d  23995  esumpinfval  24463  hasheuni  24475  measvuni  24568  elorvc  24717  ballotlemimin  24763  ballotlem7  24793  ballotth  24795  mbfposadd  26254  cover2  26415  aaitgo  27344  rfcnpre1  27666  rfcnpre2  27678  dvcosre  27717  itgsinexplem1  27724  stoweidlem27  27752  stoweidlem31  27756  stoweidlem34  27759  stoweidlem35  27760  stoweidlem59  27784  2spotmdisj  28457  bnj1204  29381
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-rab 2714
  Copyright terms: Public domain W3C validator