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

Theorem rabid 2909
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 2736 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
21abeq2i 2554 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 1756   {crab 2731
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-rab 2736
This theorem is referenced by:  rabeq2i  2981  reusv2lem4  4508  reusv2  4510  rabxfrd  4525  riotaxfrd  6095  tfis  6477  rankr1ai  8017  cfval2  8441  cflim3  8443  cflim2  8444  cfss  8446  cfslb  8447  cofsmo  8450  nnwos  10934  ramval  14081  ramub1lem1  14099  neiptopnei  18748  hauseqlcld  19231  imasnopn  19275  imasncld  19276  imasncls  19277  ptcmplem4  19639  blval2  20162  metutopOLD  20169  psmetutop  20170  mbfinf  21155  itg2monolem1  21240  lhop1  21498  rabrab  25896  rabexgfGS  25898  rabss3d  25907  fpwrelmap  26045  ordtconlem1  26366  fsumcvg4  26392  esumpinfval  26534  hasheuni  26546  measvuni  26640  eulerpartlemn  26776  elorvc  26854  ballotlemimin  26900  ballotlem7  26930  ballotth  26932  mbfposadd  28451  dvtanlem  28453  cover2  28619  aaitgo  29531  rfcnpre1  29753  rfcnpre2  29765  dvcosre  29800  itgsinexplem1  29806  stoweidlem27  29834  stoweidlem31  29838  stoweidlem34  29841  stoweidlem35  29842  stoweidlem59  29866  rusgranumwlkb0  30583  2spotmdisj  30673  numclwlk1lem2f  30697  bnj1204  32015  bj-rabtrALT  32445
  Copyright terms: Public domain W3C validator