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

Theorem rabid 2718
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 2554 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
21abeq2i 2392 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 1685   {crab 2549
This theorem is referenced by:  rabeq2i  2787  reusv2lem4  4538  reusv2  4540  rabxfrd  4555  tfis  4645  riotaxfrd  6332  rankr1ai  7466  cfval2  7882  cflim3  7884  cflim2  7885  cfss  7887  cfslb  7888  cofsmo  7891  nnwos  10282  ramval  13050  ramub1lem1  13068  hauseqlcld  17335  ptcmplem4  17744  mbfinf  19015  itg2monolem1  19100  lhop1  19356  ballotlem2  23041  ballotlemimin  23058  ballotlem7  23088  ballotth  23090  sgplpte21a  25533  cover2  25758  aaitgo  26767  rfcnpre1  27090  rfcnpre2  27102  dvcosre  27141  itgsinexplem1  27148  stoweidlem24  27173  stoweidlem27  27176  stoweidlem31  27180  stoweidlem34  27183  stoweidlem35  27184  stoweidlem54  27203  stoweidlem57  27206  stoweidlem59  27208  bnj1204  28310
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-11 1716  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1530  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-rab 2554
  Copyright terms: Public domain W3C validator