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

Theorem rabid 3430
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 3411 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
21eqabi 2882 1 (𝑥 ∈ {𝑥𝐴𝜑} ↔ (𝑥𝐴𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  wcel 2107  {crab 3410
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-12 2172  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3411
This theorem is referenced by:  rabidim1  3431  reqabi  3432  rabrab  3433  rabss3d  4044  reusv2lem4  5361  reusv2  5363  rabxfrd  5377  riotaxfrd  7353  tfis  7796  rankr1ai  9741  cfval2  10203  cflim3  10205  cflim2  10206  cfss  10208  cfslb  10209  cofsmo  10212  nnwos  12847  ramval  16887  ramub1lem1  16905  neiptopnei  22499  dissnlocfin  22896  hauseqlcld  23013  imasnopn  23057  imasncld  23058  imasncls  23059  ptcmplem4  23422  blval2  23934  psmetutop  23939  rrxbasefi  24790  mbfinf  25045  itg2monolem1  25131  lhop1  25394  ssltleft  27222  ssltright  27223  sltlpss  27258  cofcutr  27265  cofcutrtime  27268  addsproplem2  27304  rusgrnumwwlkb0  28958  difrab2  31468  eqrrabd  31472  fimarab  31601  aciunf1  31621  fpwrelmap  31692  locfinreflem  32461  zarcls  32495  ordtconnlem1  32545  fsumcvg4  32571  esumrnmpt2  32707  esumpinfval  32712  hasheuni  32724  measvuni  32853  eulerpartlemn  33021  elorvc  33099  ballotlemimin  33145  ballotlem7  33175  ballotth  33177  reprinrn  33271  reprpmtf1o  33279  reprdifc  33280  bnj1204  33664  bj-rabtrALT  35430  icorempo  35851  isbasisrelowllem1  35855  isbasisrelowllem2  35856  relowlssretop  35863  phpreu  36091  poimirlem26  36133  mbfposadd  36154  cover2  36202  aaitgo  41518  rababg  41920  nznngen  42670  rfcnpre1  43298  rfcnpre2  43310  rabidim2  43386  rabidd  43444  disjf1o  43484  mptssid  43541  infnsuprnmpt  43552  allbutfiinf  43729  supminfxr2  43778  pimxrneun  43798  fsumsupp0  43893  limsupequzmpt2  44033  liminfequzmpt2  44106  cncfshift  44189  cncfperiod  44194  dvcosre  44227  dvnprodlem1  44261  itgsinexplem1  44269  stoweidlem27  44342  stoweidlem31  44346  stoweidlem34  44349  stoweidlem35  44350  stoweidlem59  44374  fourierdlem31  44453  etransclem32  44581  etransclem35  44584  etransclem37  44586  etransclem38  44587  sge0iunmptlemre  44730  meadjiunlem  44780  ovncvrrp  44879  hoidmv1lelem1  44906  hoidmvlelem2  44911  ovnhoilem2  44917  opnvonmbllem2  44948  ovolval4lem1  44964  preimagelt  45014  preimalegt  45015  pimconstlt1  45017  pimltpnff  45018  pimrecltpos  45023  pimiooltgt  45025  preimageiingt  45035  preimaleiinlt  45036  pimgtmnff  45037  pimrecltneg  45039  sssmf  45053  smfaddlem1  45078  smflimlem2  45087  smfmullem4  45109  smflimsuplem4  45138  smflimsuplem7  45141
  Copyright terms: Public domain W3C validator