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

Theorem rabid 3114
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 2920 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
21abeq2i 2734 1 (𝑥 ∈ {𝑥𝐴𝜑} ↔ (𝑥𝐴𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384  wcel 1989  {crab 2915
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-12 2046  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1485  df-ex 1704  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-rab 2920
This theorem is referenced by:  rabidim1  3115  rabeq2i  3195  reusv2lem4  4870  reusv2  4872  rabxfrd  4887  riotaxfrd  6639  tfis  7051  rankr1ai  8658  cfval2  9079  cflim3  9081  cflim2  9082  cfss  9084  cfslb  9085  cofsmo  9088  nnwos  11752  ramval  15706  ramub1lem1  15724  neiptopnei  20930  dissnlocfin  21326  hauseqlcld  21443  imasnopn  21487  imasncld  21488  imasncls  21489  ptcmplem4  21853  blval2  22361  psmetutop  22366  mbfinf  23426  itg2monolem1  23511  lhop1  23771  rusgrnumwwlkb0  26860  rabrab  29322  difrab2  29323  rabexgfGS  29324  rabss3d  29335  fimarab  29429  aciunf1  29447  fpwrelmap  29493  locfinreflem  29892  ordtconnlem1  29955  fsumcvg4  29981  esumrnmpt2  30115  esumpinfval  30120  hasheuni  30132  measvuni  30262  eulerpartlemn  30428  elorvc  30506  ballotlemimin  30552  ballotlem7  30582  ballotth  30584  reprinrn  30681  reprpmtf1o  30689  reprdifc  30690  bnj1204  31065  bj-rabtrALT  32911  icorempt2  33179  isbasisrelowllem1  33183  isbasisrelowllem2  33184  relowlssretop  33191  phpreu  33373  poimirlem26  33415  mbfposadd  33437  cover2  33488  aaitgo  37558  rababg  37705  nznngen  38341  rfcnpre1  39004  rfcnpre2  39016  rabidim2  39110  disjf1o  39200  mptssid  39272  infnsuprnmpt  39287  allbutfiinf  39466  supminfxr2  39518  fsumsupp0  39616  limsupequzmpt2  39756  liminfequzmpt2  39823  cncfshift  39856  cncfperiod  39861  dvcosre  39895  dvnprodlem1  39930  itgsinexplem1  39938  stoweidlem27  40013  stoweidlem31  40017  stoweidlem34  40020  stoweidlem35  40021  stoweidlem59  40045  fourierdlem31  40124  etransclem32  40252  etransclem35  40255  etransclem37  40257  etransclem38  40258  rrxbasefi  40272  sge0iunmptlemre  40401  meadjiunlem  40451  ovncvrrp  40547  hoidmv1lelem1  40574  hoidmvlelem2  40579  ovnhoilem2  40585  opnvonmbllem2  40616  ovolval4lem1  40632  preimagelt  40681  preimalegt  40682  pimconstlt1  40684  pimltpnf  40685  pimrecltpos  40688  pimiooltgt  40690  preimageiingt  40699  preimaleiinlt  40700  pimrecltneg  40702  sssmf  40716  smfaddlem1  40740  smflimlem2  40749  smfmullem4  40770  smflimsuplem4  40798  smflimsuplem7  40801
  Copyright terms: Public domain W3C validator