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

Theorem rabid 3359
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 3139 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
21abeq2i 2949 1 (𝑥 ∈ {𝑥𝐴𝜑} ↔ (𝑥𝐴𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399  wcel 2114  {crab 3134
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2178  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-rab 3139
This theorem is referenced by:  rabrab  3360  rabidim1  3361  rabeq2i  3463  reusv2lem4  5279  reusv2  5281  rabxfrd  5295  riotaxfrd  7132  tfis  7554  rankr1ai  9215  cfval2  9671  cflim3  9673  cflim2  9674  cfss  9676  cfslb  9677  cofsmo  9680  nnwos  12303  ramval  16333  ramub1lem1  16351  neiptopnei  21735  dissnlocfin  22132  hauseqlcld  22249  imasnopn  22293  imasncld  22294  imasncls  22295  ptcmplem4  22658  blval2  23167  psmetutop  23172  rrxbasefi  24012  mbfinf  24267  itg2monolem1  24352  lhop1  24615  rusgrnumwwlkb0  27755  difrab2  30266  eqrrabd  30270  rabss3d  30283  fimarab  30398  aciunf1  30416  fpwrelmap  30479  locfinreflem  31162  zarcls  31196  ordtconnlem1  31241  fsumcvg4  31267  esumrnmpt2  31401  esumpinfval  31406  hasheuni  31418  measvuni  31547  eulerpartlemn  31713  elorvc  31791  ballotlemimin  31837  ballotlem7  31867  ballotth  31869  reprinrn  31963  reprpmtf1o  31971  reprdifc  31972  bnj1204  32358  bj-rabtrALT  34334  icorempo  34729  isbasisrelowllem1  34733  isbasisrelowllem2  34734  relowlssretop  34741  phpreu  35000  poimirlem26  35042  mbfposadd  35063  cover2  35111  aaitgo  40037  rababg  40204  nznngen  40955  rfcnpre1  41583  rfcnpre2  41595  rabidim2  41675  disjf1o  41757  mptssid  41816  infnsuprnmpt  41827  allbutfiinf  41997  supminfxr2  42048  fsumsupp0  42160  limsupequzmpt2  42300  liminfequzmpt2  42373  cncfshift  42456  cncfperiod  42461  dvcosre  42494  dvnprodlem1  42528  itgsinexplem1  42536  stoweidlem27  42609  stoweidlem31  42613  stoweidlem34  42616  stoweidlem35  42617  stoweidlem59  42641  fourierdlem31  42720  etransclem32  42848  etransclem35  42851  etransclem37  42853  etransclem38  42854  sge0iunmptlemre  42994  meadjiunlem  43044  ovncvrrp  43143  hoidmv1lelem1  43170  hoidmvlelem2  43175  ovnhoilem2  43181  opnvonmbllem2  43212  ovolval4lem1  43228  preimagelt  43277  preimalegt  43278  pimconstlt1  43280  pimltpnf  43281  pimrecltpos  43284  pimiooltgt  43286  preimageiingt  43295  preimaleiinlt  43296  pimrecltneg  43298  sssmf  43312  smfaddlem1  43336  smflimlem2  43345  smfmullem4  43366  smflimsuplem4  43394  smflimsuplem7  43397
  Copyright terms: Public domain W3C validator