Theorem rabid 3453

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 3434	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
2	1	eqabri 2878	1 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))

Syntax hints:   ↔ wb 205   ∧ wa 397   ∈ wcel 2107  {crab 3433

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434

This theorem is referenced by:  rabidim1  3454  reqabi  3455  rabrab  3456  rabss3d  4078  reusv2lem4  5398  reusv2  5400  rabxfrd  5414  riotaxfrd  7395  tfis  7839  rankr1ai  9789  cfval2  10251  cflim3  10253  cflim2  10254  cfss  10256  cfslb  10257  cofsmo  10260  nnwos  12895  ramval  16937  ramub1lem1  16955  neiptopnei  22618  dissnlocfin  23015  hauseqlcld  23132  imasnopn  23176  imasncld  23177  imasncls  23178  ptcmplem4  23541  blval2  24053  psmetutop  24058  rrxbasefi  24909  mbfinf  25164  itg2monolem1  25250  lhop1  25513  ssltleft  27345  ssltright  27346  sltlpss  27381  cofcutr  27391  cofcutrtime  27394  addsproplem2  27434  rusgrnumwwlkb0  29205  difrab2  31716  eqrrabd  31719  fimarab  31846  aciunf1  31866  fpwrelmap  31936  locfinreflem  32758  zarcls  32792  ordtconnlem1  32842  fsumcvg4  32868  esumrnmpt2  33004  esumpinfval  33009  hasheuni  33021  measvuni  33150  eulerpartlemn  33318  elorvc  33396  ballotlemimin  33442  ballotlem7  33472  ballotth  33474  reprinrn  33568  reprpmtf1o  33576  reprdifc  33577  bnj1204  33961  bj-rabtrALT  35749  icorempo  36170  isbasisrelowllem1  36174  isbasisrelowllem2  36175  relowlssretop  36182  phpreu  36410  poimirlem26  36452  mbfposadd  36473  cover2  36521  aaitgo  41837  rababg  42258  nznngen  43008  rfcnpre1  43636  rfcnpre2  43648  rabidim2  43724  rabidd  43782  disjf1o  43822  mptssid  43878  infnsuprnmpt  43889  allbutfiinf  44065  supminfxr2  44114  pimxrneun  44134  fsumsupp0  44229  limsupequzmpt2  44369  liminfequzmpt2  44442  cncfshift  44525  cncfperiod  44530  dvcosre  44563  dvnprodlem1  44597  itgsinexplem1  44605  stoweidlem27  44678  stoweidlem31  44682  stoweidlem34  44685  stoweidlem35  44686  stoweidlem59  44710  fourierdlem31  44789  etransclem32  44917  etransclem35  44920  etransclem37  44922  etransclem38  44923  sge0iunmptlemre  45066  meadjiunlem  45116  ovncvrrp  45215  hoidmv1lelem1  45242  hoidmvlelem2  45247  ovnhoilem2  45253  opnvonmbllem2  45284  ovolval4lem1  45300  preimagelt  45350  preimalegt  45351  pimconstlt1  45353  pimltpnff  45354  pimrecltpos  45359  pimiooltgt  45361  preimageiingt  45371  preimaleiinlt  45372  pimgtmnff  45373  pimrecltneg  45375  sssmf  45389  smfaddlem1  45414  smflimlem2  45423  smfmullem4  45445  smflimsuplem4  45474  smflimsuplem7  45477