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

Theorem rabid 2729
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 2565 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
21abeq2i 2403 1  |-  ( x  e.  { x  e.  A  |  ph }  <->  ( x  e.  A  /\  ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    e. wcel 1696   {crab 2560
This theorem is referenced by:  rabeq2i  2798  reusv2lem4  4554  reusv2  4556  rabxfrd  4571  tfis  4661  riotaxfrd  6352  rankr1ai  7486  cfval2  7902  cflim3  7904  cflim2  7905  cfss  7907  cfslb  7908  cofsmo  7911  nnwos  10302  ramval  13071  ramub1lem1  13089  hauseqlcld  17356  ptcmplem4  17765  mbfinf  19036  itg2monolem1  19121  lhop1  19377  ballotlem2  23063  ballotlemimin  23080  ballotlem7  23110  ballotth  23112  rabss3d  23152  rabexgfGS  23187  esumpinfval  23456  hasheuni  23468  measvuni  23557  elorvc  23675  sgplpte21a  26236  cover2  26461  aaitgo  27470  rfcnpre1  27793  rfcnpre2  27805  dvcosre  27844  itgsinexplem1  27851  stoweidlem24  27876  stoweidlem27  27879  stoweidlem31  27883  stoweidlem34  27886  stoweidlem35  27887  stoweidlem54  27906  stoweidlem57  27909  stoweidlem59  27911  nbusgra  28277  bnj1204  29358
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-rab 2565
  Copyright terms: Public domain W3C validator