Theorem rabid 3411

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  {crab 3390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391

This theorem is referenced by:  rabidim1  3412  reqabi  3413  rabrab  3414  rabss3d  4022  eqrrabd  4027  reusv2lem4  5339  reusv2  5341  rabxfrd  5355  fimarab  6909  riotaxfrd  7352  tfis  7800  rankr1ai  9716  cfval2  10176  cflim3  10178  cflim2  10179  cfss  10181  cfslb  10182  cofsmo  10185  nnwos  12859  ramval  16973  ramub1lem1  16991  neiptopnei  23110  dissnlocfin  23507  hauseqlcld  23624  imasnopn  23668  imasncld  23669  imasncls  23670  ptcmplem4  24033  blval2  24540  psmetutop  24545  rrxbasefi  25390  mbfinf  25645  itg2monolem1  25730  lhop1  25994  sltsleft  27869  sltsright  27870  ltslpss  27917  cofcutr  27933  cofcutrtime  27936  addsproplem2  27979  rusgrnumwwlkb0  30060  difrab2  32585  aciunf1  32754  fpwrelmap  32824  cntrval2  33250  ply1mulrtss  33660  algextdeglem6  33885  constrfin  33909  locfinreflem  34003  zarcls  34037  ordtconnlem1  34087  fsumcvg4  34113  esumrnmpt2  34231  esumpinfval  34236  hasheuni  34248  measvuni  34377  eulerpartlemn  34544  elorvc  34623  ballotlemimin  34669  ballotlem7  34699  ballotth  34701  reprinrn  34781  reprpmtf1o  34789  reprdifc  34790  bnj1204  35173  bj-rabtrALT  37257  icorempo  37684  isbasisrelowllem1  37688  isbasisrelowllem2  37689  relowlssretop  37696  phpreu  37942  poimirlem26  37984  mbfposadd  38005  cover2  38053  aaitgo  43611  rababg  44022  nznngen  44764  permaxsep  45455  rfcnpre1  45471  rfcnpre2  45483  rabidim2  45553  rabidd  45606  disjf1o  45642  mptssid  45691  infnsuprnmpt  45700  allbutfiinf  45869  supminfxr2  45918  pimxrneun  45937  fsumsupp0  46029  limsupequzmpt2  46167  liminfequzmpt2  46240  cncfshift  46323  cncfperiod  46328  dvcosre  46361  dvnprodlem1  46395  itgsinexplem1  46403  stoweidlem27  46476  stoweidlem31  46480  stoweidlem34  46483  stoweidlem35  46484  stoweidlem59  46508  fourierdlem31  46587  etransclem32  46715  etransclem35  46718  etransclem37  46720  etransclem38  46721  sge0iunmptlemre  46864  meadjiunlem  46914  ovncvrrp  47013  hoidmv1lelem1  47040  hoidmvlelem2  47045  ovnhoilem2  47051  opnvonmbllem2  47082  ovolval4lem1  47098  preimagelt  47148  preimalegt  47149  pimconstlt1  47151  pimltpnff  47152  pimrecltpos  47157  pimgtmnff  47171  pimrecltneg  47173  sssmf  47187  smfaddlem1  47212  smflimlem2  47221  smfmullem4  47243  smflimsuplem4  47272  smflimsuplem7  47275