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

Theorem rabid 3091
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 2901 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
21abeq2i 2718 1 (𝑥 ∈ {𝑥𝐴𝜑} ↔ (𝑥𝐴𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wa 382  wcel 1976  {crab 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-12 2032  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-an 384  df-tru 1477  df-ex 1695  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-rab 2901
This theorem is referenced by:  rabeq2i  3166  reusv2lem4  4790  reusv2  4792  rabxfrd  4807  riotaxfrd  6516  tfis  6920  rankr1ai  8518  cfval2  8939  cflim3  8941  cflim2  8942  cfss  8944  cfslb  8945  cofsmo  8948  nnwos  11584  ramval  15493  ramub1lem1  15511  neiptopnei  20685  dissnlocfin  21081  hauseqlcld  21198  imasnopn  21242  imasncld  21243  imasncls  21244  ptcmplem4  21608  blval2  22115  psmetutop  22120  mbfinf  23152  itg2monolem1  23237  lhop1  23495  rusgranumwlkb0  26243  2spotmdisj  26358  numclwlk1lem2f  26382  rabrab  28525  rabexgfGS  28528  rabss3d  28539  fimarab  28628  aciunf1  28648  fpwrelmap  28699  locfinreflem  29038  ordtconlem1  29101  fsumcvg4  29127  esumrnmpt2  29260  esumpinfval  29265  hasheuni  29277  measvuni  29407  eulerpartlemn  29573  elorvc  29651  ballotlemimin  29697  ballotlem7  29727  ballotth  29729  bnj1204  30137  bj-rabtrALT  31919  icorempt2  32175  isbasisrelowllem1  32179  isbasisrelowllem2  32180  relowlssretop  32187  phpreu  32363  poimirlem26  32405  mbfposadd  32427  cover2  32478  aaitgo  36551  rababg  36698  nznngen  37337  rfcnpre1  38001  rfcnpre2  38013  rabid3  38085  rabidim2  38113  rabidim1  38118  disjf1o  38173  fsumsupp0  38446  cncfshift  38560  cncfperiod  38565  dvcosre  38600  dvnprodlem1  38637  itgsinexplem1  38646  stoweidlem27  38721  stoweidlem31  38725  stoweidlem34  38728  stoweidlem35  38729  stoweidlem59  38753  fourierdlem31  38832  etransclem32  38960  etransclem35  38963  etransclem37  38965  etransclem38  38966  rrxbasefi  38980  sge0iunmptlemre  39109  meadjiunlem  39159  ovncvrrp  39255  hoidmv1lelem1  39282  hoidmvlelem2  39287  ovnhoilem2  39293  opnvonmbllem2  39324  ovolval4lem1  39340  preimagelt  39390  preimalegt  39391  pimconstlt1  39393  pimltpnf  39394  pimrecltpos  39397  pimiooltgt  39399  preimageiingt  39408  preimaleiinlt  39409  pimrecltneg  39411  sssmf  39426  smfaddlem1  39450  smflimlem2  39459  smfmullem4  39480  rusgrnumwwlkb0  41173  av-numclwlk1lem2f  41521
  Copyright terms: Public domain W3C validator