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  4080  reusv2lem4  5400  reusv2  5402  rabxfrd  5416  riotaxfrd  7400  tfis  7844  rankr1ai  9793  cfval2  10255  cflim3  10257  cflim2  10258  cfss  10260  cfslb  10261  cofsmo  10264  nnwos  12899  ramval  16941  ramub1lem1  16959  neiptopnei  22636  dissnlocfin  23033  hauseqlcld  23150  imasnopn  23194  imasncld  23195  imasncls  23196  ptcmplem4  23559  blval2  24071  psmetutop  24076  rrxbasefi  24927  mbfinf  25182  itg2monolem1  25268  lhop1  25531  ssltleft  27365  ssltright  27366  sltlpss  27401  cofcutr  27411  cofcutrtime  27414  addsproplem2  27454  rusgrnumwwlkb0  29225  difrab2  31738  eqrrabd  31741  fimarab  31868  aciunf1  31888  fpwrelmap  31958  locfinreflem  32820  zarcls  32854  ordtconnlem1  32904  fsumcvg4  32930  esumrnmpt2  33066  esumpinfval  33071  hasheuni  33083  measvuni  33212  eulerpartlemn  33380  elorvc  33458  ballotlemimin  33504  ballotlem7  33534  ballotth  33536  reprinrn  33630  reprpmtf1o  33638  reprdifc  33639  bnj1204  34023  bj-rabtrALT  35811  icorempo  36232  isbasisrelowllem1  36236  isbasisrelowllem2  36237  relowlssretop  36244  phpreu  36472  poimirlem26  36514  mbfposadd  36535  cover2  36583  aaitgo  41904  rababg  42325  nznngen  43075  rfcnpre1  43703  rfcnpre2  43715  rabidim2  43791  rabidd  43849  disjf1o  43889  mptssid  43944  infnsuprnmpt  43954  allbutfiinf  44130  supminfxr2  44179  pimxrneun  44199  fsumsupp0  44294  limsupequzmpt2  44434  liminfequzmpt2  44507  cncfshift  44590  cncfperiod  44595  dvcosre  44628  dvnprodlem1  44662  itgsinexplem1  44670  stoweidlem27  44743  stoweidlem31  44747  stoweidlem34  44750  stoweidlem35  44751  stoweidlem59  44775  fourierdlem31  44854  etransclem32  44982  etransclem35  44985  etransclem37  44987  etransclem38  44988  sge0iunmptlemre  45131  meadjiunlem  45181  ovncvrrp  45280  hoidmv1lelem1  45307  hoidmvlelem2  45312  ovnhoilem2  45318  opnvonmbllem2  45349  ovolval4lem1  45365  preimagelt  45415  preimalegt  45416  pimconstlt1  45418  pimltpnff  45419  pimrecltpos  45424  pimiooltgt  45426  preimageiingt  45436  preimaleiinlt  45437  pimgtmnff  45438  pimrecltneg  45440  sssmf  45454  smfaddlem1  45479  smflimlem2  45488  smfmullem4  45510  smflimsuplem4  45539  smflimsuplem7  45542