Theorem rabid 3454

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

Step	Hyp	Ref	Expression
1		df-rab 3433	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
2	1	eqabri 2882	1 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2105  {crab 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-12 2174  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433

This theorem is referenced by:  rabidim1  3455  reqabi  3456  rabrab  3457  rabss3d  4090  eqrrabd  4095  reusv2lem4  5406  reusv2  5408  rabxfrd  5422  fimarab  6982  riotaxfrd  7421  tfis  7875  rankr1ai  9835  cfval2  10297  cflim3  10299  cflim2  10300  cfss  10302  cfslb  10303  cofsmo  10306  nnwos  12954  ramval  17041  ramub1lem1  17059  neiptopnei  23155  dissnlocfin  23552  hauseqlcld  23669  imasnopn  23713  imasncld  23714  imasncls  23715  ptcmplem4  24078  blval2  24590  psmetutop  24595  rrxbasefi  25457  mbfinf  25713  itg2monolem1  25799  lhop1  26067  ssltleft  27923  ssltright  27924  sltlpss  27959  cofcutr  27972  cofcutrtime  27975  addsproplem2  28017  rusgrnumwwlkb0  30000  difrab2  32525  aciunf1  32679  fpwrelmap  32750  ply1mulrtss  33585  algextdeglem6  33727  constrfin  33750  locfinreflem  33800  zarcls  33834  ordtconnlem1  33884  fsumcvg4  33910  esumrnmpt2  34048  esumpinfval  34053  hasheuni  34065  measvuni  34194  eulerpartlemn  34362  elorvc  34440  ballotlemimin  34486  ballotlem7  34516  ballotth  34518  reprinrn  34611  reprpmtf1o  34619  reprdifc  34620  bnj1204  35004  bj-rabtrALT  36913  icorempo  37333  isbasisrelowllem1  37337  isbasisrelowllem2  37338  relowlssretop  37345  phpreu  37590  poimirlem26  37632  mbfposadd  37653  cover2  37701  aaitgo  43150  rababg  43563  nznngen  44311  rfcnpre1  44956  rfcnpre2  44968  rabidim2  45041  rabidd  45097  disjf1o  45133  mptssid  45184  infnsuprnmpt  45194  allbutfiinf  45369  supminfxr2  45418  pimxrneun  45438  fsumsupp0  45533  limsupequzmpt2  45673  liminfequzmpt2  45746  cncfshift  45829  cncfperiod  45834  dvcosre  45867  dvnprodlem1  45901  itgsinexplem1  45909  stoweidlem27  45982  stoweidlem31  45986  stoweidlem34  45989  stoweidlem35  45990  stoweidlem59  46014  fourierdlem31  46093  etransclem32  46221  etransclem35  46224  etransclem37  46226  etransclem38  46227  sge0iunmptlemre  46370  meadjiunlem  46420  ovncvrrp  46519  hoidmv1lelem1  46546  hoidmvlelem2  46551  ovnhoilem2  46557  opnvonmbllem2  46588  ovolval4lem1  46604  preimagelt  46654  preimalegt  46655  pimconstlt1  46657  pimltpnff  46658  pimrecltpos  46663  pimiooltgt  46665  preimageiingt  46675  preimaleiinlt  46676  pimgtmnff  46677  pimrecltneg  46679  sssmf  46693  smfaddlem1  46718  smflimlem2  46727  smfmullem4  46749  smflimsuplem4  46778  smflimsuplem7  46781