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

Theorem rabid 2716
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 2552 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
21abeq2i 2390 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 1684   {crab 2547
This theorem is referenced by:  rabeq2i  2785  reusv2lem4  4538  reusv2  4540  rabxfrd  4555  tfis  4645  riotaxfrd  6336  rankr1ai  7470  cfval2  7886  cflim3  7888  cflim2  7889  cfss  7891  cfslb  7892  cofsmo  7895  nnwos  10286  ramval  13055  ramub1lem1  13073  hauseqlcld  17340  ptcmplem4  17749  mbfinf  19020  itg2monolem1  19105  lhop1  19361  ballotlem2  23047  ballotlemimin  23064  ballotlem7  23094  ballotth  23096  rabss3d  23136  rabexgfGS  23171  esumpinfval  23441  hasheuni  23453  measvuni  23542  elorvc  23660  sgplpte21a  26133  cover2  26358  aaitgo  27367  rfcnpre1  27690  rfcnpre2  27702  dvcosre  27741  itgsinexplem1  27748  stoweidlem24  27773  stoweidlem27  27776  stoweidlem31  27780  stoweidlem34  27783  stoweidlem35  27784  stoweidlem54  27803  stoweidlem57  27806  stoweidlem59  27808  nbusgra  28143  bnj1204  29042
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-rab 2552
  Copyright terms: Public domain W3C validator