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

Theorem rabid 3145
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 2950 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
21abeq2i 2764 1 (𝑥 ∈ {𝑥𝐴𝜑} ↔ (𝑥𝐴𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  wcel 2030  {crab 2945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-12 2087  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-tru 1526  df-ex 1745  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-rab 2950
This theorem is referenced by:  rabrab  3146  rabidim1  3147  rabeq2i  3228  reusv2lem4  4902  reusv2  4904  rabxfrd  4919  riotaxfrd  6682  tfis  7096  rankr1ai  8699  cfval2  9120  cflim3  9122  cflim2  9123  cfss  9125  cfslb  9126  cofsmo  9129  nnwos  11793  ramval  15759  ramub1lem1  15777  neiptopnei  20984  dissnlocfin  21380  hauseqlcld  21497  imasnopn  21541  imasncld  21542  imasncls  21543  ptcmplem4  21906  blval2  22414  psmetutop  22419  mbfinf  23477  itg2monolem1  23562  lhop1  23822  rusgrnumwwlkb0  26938  difrab2  29465  rabexgfGS  29466  rabss3d  29477  fimarab  29573  aciunf1  29591  fpwrelmap  29636  locfinreflem  30035  ordtconnlem1  30098  fsumcvg4  30124  esumrnmpt2  30258  esumpinfval  30263  hasheuni  30275  measvuni  30405  eulerpartlemn  30571  elorvc  30649  ballotlemimin  30695  ballotlem7  30725  ballotth  30727  reprinrn  30824  reprpmtf1o  30832  reprdifc  30833  bnj1204  31206  bj-rabtrALT  33052  icorempt2  33329  isbasisrelowllem1  33333  isbasisrelowllem2  33334  relowlssretop  33341  phpreu  33523  poimirlem26  33565  mbfposadd  33587  cover2  33638  aaitgo  38049  rababg  38196  nznngen  38832  rfcnpre1  39492  rfcnpre2  39504  rabidim2  39598  disjf1o  39692  mptssid  39764  infnsuprnmpt  39779  allbutfiinf  39960  supminfxr2  40012  fsumsupp0  40128  limsupequzmpt2  40268  liminfequzmpt2  40341  cncfshift  40405  cncfperiod  40410  dvcosre  40444  dvnprodlem1  40479  itgsinexplem1  40487  stoweidlem27  40562  stoweidlem31  40566  stoweidlem34  40569  stoweidlem35  40570  stoweidlem59  40594  fourierdlem31  40673  etransclem32  40801  etransclem35  40804  etransclem37  40806  etransclem38  40807  rrxbasefi  40821  sge0iunmptlemre  40950  meadjiunlem  41000  ovncvrrp  41099  hoidmv1lelem1  41126  hoidmvlelem2  41131  ovnhoilem2  41137  opnvonmbllem2  41168  ovolval4lem1  41184  preimagelt  41233  preimalegt  41234  pimconstlt1  41236  pimltpnf  41237  pimrecltpos  41240  pimiooltgt  41242  preimageiingt  41251  preimaleiinlt  41252  pimrecltneg  41254  sssmf  41268  smfaddlem1  41292  smflimlem2  41301  smfmullem4  41322  smflimsuplem4  41350  smflimsuplem7  41353
  Copyright terms: Public domain W3C validator