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

Theorem rabid 2959
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 2741 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
21abeq2i 2509 1  |-  ( x  e.  { x  e.  A  |  ph }  <->  ( x  e.  A  /\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 367    e. wcel 1826   {crab 2736
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-12 1862  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-rab 2741
This theorem is referenced by:  rabeq2i  3031  reusv2lem4  4569  reusv2  4571  rabxfrd  4583  riotaxfrd  6188  tfis  6588  rankr1ai  8129  cfval2  8553  cflim3  8555  cflim2  8556  cfss  8558  cfslb  8559  cofsmo  8562  nnwos  11068  ramval  14528  ramub1lem1  14546  neiptopnei  19719  dissnlocfin  20115  hauseqlcld  20232  imasnopn  20276  imasncld  20277  imasncls  20278  ptcmplem4  20640  blval2  21163  metutopOLD  21170  psmetutop  21171  mbfinf  22157  itg2monolem1  22242  lhop1  22500  rusgranumwlkb0  25074  2spotmdisj  25189  numclwlk1lem2f  25213  rabrab  27516  rabexgfGS  27519  rabss3d  27530  fimarab  27623  aciunf1  27649  fpwrelmap  27706  locfinreflem  27997  ordtconlem1  28060  fsumcvg4  28086  esumrnmpt2  28216  esumpinfval  28221  hasheuni  28233  measvuni  28341  eulerpartlemn  28503  elorvc  28581  ballotlemimin  28627  ballotlem7  28657  ballotth  28659  mbfposadd  30227  dvtanlemOLD  30230  cover2  30370  aaitgo  31279  nznngen  31389  rfcnpre1  31561  rfcnpre2  31573  cncfshift  31842  cncfperiod  31847  dvcosre  31872  dvnprodlem1  31909  itgsinexplem1  31918  stoweidlem27  31975  stoweidlem31  31979  stoweidlem34  31982  stoweidlem35  31983  stoweidlem59  32007  fourierdlem31  32086  etransclem32  32215  etransclem35  32218  etransclem37  32220  etransclem38  32221  bnj1204  34415  bj-rabtrALT  34846
  Copyright terms: Public domain W3C validator