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

Theorem rabid 2691
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 2527 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
21abeq2i 2365 1  |-  ( x  e.  { x  e.  A  |  ph }  <->  ( x  e.  A  /\  ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360    e. wcel 1621   {crab 2522
This theorem is referenced by:  rabeq2i  2760  reusv2lem4  4510  reusv2  4512  rabxfrd  4527  tfis  4617  riotaxfrd  6304  rankr1ai  7438  cfval2  7854  cflim3  7856  cflim2  7857  cfss  7859  cfslb  7860  cofsmo  7863  nnwos  10253  ramval  13017  ramub1lem1  13035  hauseqlcld  17302  ptcmplem4  17711  mbfinf  18982  itg2monolem1  19067  lhop1  19323  ballotlem2  23008  ballotlemimin  23025  ballotlem7  23055  ballotth  23057  sgplpte21a  25500  cover2  25725  aaitgo  26734  rfcnpre1  27058  rfcnpre2  27070  stoweidlem24  27108  stoweidlem27  27111  stoweidlem31  27115  stoweidlem34  27118  stoweidlem35  27119  stoweidlem54  27138  stoweidlem57  27141  stoweidlem59  27143  bnj1204  28091
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-12o 1664  ax-9 1684  ax-4 1692  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-rab 2527
  Copyright terms: Public domain W3C validator