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

Theorem rabid 3038
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 2823 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
21abeq2i 2594 1  |-  ( x  e.  { x  e.  A  |  ph }  <->  ( x  e.  A  /\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    e. wcel 1767   {crab 2818
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-12 1803  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-rab 2823
This theorem is referenced by:  rabeq2i  3110  reusv2lem4  4651  reusv2  4653  rabxfrd  4668  riotaxfrd  6275  tfis  6668  rankr1ai  8215  cfval2  8639  cflim3  8641  cflim2  8642  cfss  8644  cfslb  8645  cofsmo  8648  nnwos  11148  ramval  14384  ramub1lem1  14402  neiptopnei  19415  hauseqlcld  19898  imasnopn  19942  imasncld  19943  imasncls  19944  ptcmplem4  20306  blval2  20829  metutopOLD  20836  psmetutop  20837  mbfinf  21823  itg2monolem1  21908  lhop1  22166  rusgranumwlkb0  24645  2spotmdisj  24761  numclwlk1lem2f  24785  rabrab  27091  rabexgfGS  27093  rabss3d  27102  fpwrelmap  27244  ordtconlem1  27558  fsumcvg4  27584  esumpinfval  27735  hasheuni  27747  measvuni  27841  eulerpartlemn  27976  elorvc  28054  ballotlemimin  28100  ballotlem7  28130  ballotth  28132  mbfposadd  29655  dvtanlem  29657  cover2  29823  aaitgo  30732  nznngen  30837  rfcnpre1  30988  rfcnpre2  31000  iccintsng  31143  cncfshift  31228  cncfperiod  31233  dvcosre  31255  itgsinexplem1  31287  stoweidlem27  31343  stoweidlem31  31347  stoweidlem34  31350  stoweidlem35  31351  stoweidlem59  31375  fourierdlem31  31454  bnj1204  33156  bj-rabtrALT  33588
  Copyright terms: Public domain W3C validator