Theorem rabid 3116

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

Step	Hyp	Ref	Expression
1		df-rab 2921	. 2 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
2	1	abeq2i 2735	1 |- ( x e. { x e. A | ph } <-> ( x e. A /\ ph ) )

Syntax hints:   <-> wb 196   /\ wa 384   e. wcel 1990   {crab 2916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1486  df-ex 1705  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-rab 2921

This theorem is referenced by:  rabidim1  3117  rabeq2i  3197  reusv2lem4  4872  reusv2  4874  rabxfrd  4889  riotaxfrd  6642  tfis  7054  rankr1ai  8661  cfval2  9082  cflim3  9084  cflim2  9085  cfss  9087  cfslb  9088  cofsmo  9091  nnwos  11755  ramval  15712  ramub1lem1  15730  neiptopnei  20936  dissnlocfin  21332  hauseqlcld  21449  imasnopn  21493  imasncld  21494  imasncls  21495  ptcmplem4  21859  blval2  22367  psmetutop  22372  mbfinf  23432  itg2monolem1  23517  lhop1  23777  rusgrnumwwlkb0  26866  rabrab  29338  difrab2  29339  rabexgfGS  29340  rabss3d  29351  fimarab  29445  aciunf1  29463  fpwrelmap  29508  locfinreflem  29907  ordtconnlem1  29970  fsumcvg4  29996  esumrnmpt2  30130  esumpinfval  30135  hasheuni  30147  measvuni  30277  eulerpartlemn  30443  elorvc  30521  ballotlemimin  30567  ballotlem7  30597  ballotth  30599  reprinrn  30696  reprpmtf1o  30704  reprdifc  30705  bnj1204  31080  bj-rabtrALT  32927  icorempt2  33199  isbasisrelowllem1  33203  isbasisrelowllem2  33204  relowlssretop  33211  phpreu  33393  poimirlem26  33435  mbfposadd  33457  cover2  33508  aaitgo  37732  rababg  37879  nznngen  38515  rfcnpre1  39178  rfcnpre2  39190  rabidim2  39284  disjf1o  39378  mptssid  39450  infnsuprnmpt  39465  allbutfiinf  39647  supminfxr2  39699  fsumsupp0  39810  limsupequzmpt2  39950  liminfequzmpt2  40023  cncfshift  40087  cncfperiod  40092  dvcosre  40126  dvnprodlem1  40161  itgsinexplem1  40169  stoweidlem27  40244  stoweidlem31  40248  stoweidlem34  40251  stoweidlem35  40252  stoweidlem59  40276  fourierdlem31  40355  etransclem32  40483  etransclem35  40486  etransclem37  40488  etransclem38  40489  rrxbasefi  40503  sge0iunmptlemre  40632  meadjiunlem  40682  ovncvrrp  40778  hoidmv1lelem1  40805  hoidmvlelem2  40810  ovnhoilem2  40816  opnvonmbllem2  40847  ovolval4lem1  40863  preimagelt  40912  preimalegt  40913  pimconstlt1  40915  pimltpnf  40916  pimrecltpos  40919  pimiooltgt  40921  preimageiingt  40930  preimaleiinlt  40931  pimrecltneg  40933  sssmf  40947  smfaddlem1  40971  smflimlem2  40980  smfmullem4  41001  smflimsuplem4  41029  smflimsuplem7  41032