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

Theorem rabid 2979
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 2758 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
21abeq2i 2574 1  |-  ( x  e.  { x  e.  A  |  ph }  <->  ( x  e.  A  /\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    /\ wa 375    e. wcel 1898   {crab 2753
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-12 1944  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-rab 2758
This theorem is referenced by:  rabeq2i  3054  reusv2lem4  4621  reusv2  4623  rabxfrd  4635  riotaxfrd  6307  tfis  6708  rankr1ai  8295  cfval2  8716  cflim3  8718  cflim2  8719  cfss  8721  cfslb  8722  cofsmo  8725  nnwos  11255  ramval  15009  ramvalOLD  15010  ramub1lem1  15033  neiptopnei  20197  dissnlocfin  20593  hauseqlcld  20710  imasnopn  20754  imasncld  20755  imasncls  20756  ptcmplem4  21119  blval2  21626  psmetutop  21631  mbfinf  22670  mbfinfOLD  22671  itg2monolem1  22757  lhop1  23015  rusgranumwlkb0  25730  2spotmdisj  25845  numclwlk1lem2f  25869  rabrab  28183  rabexgfGS  28186  rabss3d  28197  fimarab  28293  aciunf1  28314  fpwrelmap  28367  locfinreflem  28716  ordtconlem1  28779  fsumcvg4  28805  esumrnmpt2  28938  esumpinfval  28943  hasheuni  28955  measvuni  29085  eulerpartlemn  29263  elorvc  29341  ballotlemimin  29387  ballotlem7  29417  ballotth  29419  ballotlemiminOLD  29425  ballotlem7OLD  29455  ballotthOLD  29457  bnj1204  29870  bj-rabtrALT  31579  icorempt2  31799  isbasisrelowllem1  31803  isbasisrelowllem2  31804  relowlssretop  31811  phpreu  31974  poimirlem26  32011  mbfposadd  32033  dvtanlemOLD  32036  cover2  32085  aaitgo  36073  rababg  36224  nznngen  36709  rfcnpre1  37380  rfcnpre2  37392  disjf1o  37504  fsumsupp0  37695  cncfshift  37789  cncfperiod  37794  dvcosre  37819  dvnprodlem1  37859  itgsinexplem1  37868  stoweidlem27  37925  stoweidlem31  37930  stoweidlem34  37933  stoweidlem35  37934  stoweidlem59  37958  fourierdlem31  38038  fourierdlem31OLD  38039  etransclem32  38169  etransclem35  38172  etransclem37  38174  etransclem38  38175  rrxbasefi  38190  sge0iunmptlemre  38295  meadjiunlem  38341  ovncvrrp  38424  hoidmv1lelem1  38451  hoidmvlelem2  38456  ovnhoilem2  38462  opnvonmbllem2  38493
  Copyright terms: Public domain W3C validator