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

Theorem rabid 3034
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

Proof of Theorem rabid
StepHypRef Expression
1 df-rab 2816 . 2
21abeq2i 2584 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  e.wcel 1818  {crab 2811
This theorem is referenced by:  rabeq2i  3106  reusv2lem4  4656  reusv2  4658  rabxfrd  4673  riotaxfrd  6288  tfis  6689  rankr1ai  8237  cfval2  8661  cflim3  8663  cflim2  8664  cfss  8666  cfslb  8667  cofsmo  8670  nnwos  11178  ramval  14526  ramub1lem1  14544  neiptopnei  19633  dissnlocfin  20030  hauseqlcld  20147  imasnopn  20191  imasncld  20192  imasncls  20193  ptcmplem4  20555  blval2  21078  metutopOLD  21085  psmetutop  21086  mbfinf  22072  itg2monolem1  22157  lhop1  22415  rusgranumwlkb0  24953  2spotmdisj  25068  numclwlk1lem2f  25092  rabrab  27399  rabexgfGS  27401  rabss3d  27412  fimarab  27483  fpwrelmap  27556  locfinreflem  27843  ordtconlem1  27906  fsumcvg4  27932  esumpinfval  28079  hasheuni  28091  measvuni  28185  eulerpartlemn  28320  elorvc  28398  ballotlemimin  28444  ballotlem7  28474  ballotth  28476  mbfposadd  30062  dvtanlem  30064  cover2  30204  aaitgo  31111  nznngen  31221  rfcnpre1  31394  rfcnpre2  31406  cncfshift  31676  cncfperiod  31681  dvcosre  31706  dvnprodlem1  31743  itgsinexplem1  31752  stoweidlem27  31809  stoweidlem31  31813  stoweidlem34  31816  stoweidlem35  31817  stoweidlem59  31841  fourierdlem31  31920  etransclem32  32049  etransclem35  32052  etransclem37  32054  etransclem38  32055  bnj1204  34068  bj-rabtrALT  34498
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-rab 2816
  Copyright terms: Public domain W3C validator