Theorem rabid 3437

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

Syntax hints:   ↔ wb 209   ∧ wa 400   ∈ wcel 2143  {crab 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417

This theorem is referenced by:  rabidim1  3438  reqabi  3439  rabrab  3440  rabss3d  4035  eqrrabd  4040  reusv2lem4  5372  reusv2  5374  rabxfrd  5388  fimarab  6955  riotaxfrd  7401  tfis  7847  rankr1ai  9766  cfval2  10239  cflim3  10241  cflim2  10242  cfss  10244  cfslb  10245  cofsmo  10248  nnwos  12934  ramval  17063  ramub1lem1  17081  rspsn0  21372  neiptopnei  23289  dissnlocfin  23686  hauseqlcld  23803  imasnopn  23847  imasncld  23848  imasncls  23849  ptcmplem4  24212  blval2  24719  psmetutop  24724  rrxbasefi  25569  mbfinf  25824  itg2monolem1  25909  lhop1  26173  sltsleft  28053  sltsright  28054  ltslpss  28101  cofcutr  28117  cofcutrtime  28120  addsproplem2  28163  rusgrnumwwlkb0  30323  difrab2  32844  aciunf1  33008  fpwrelmap  33078  cntrval2  33491  ply1mulrtss  33872  algextdeglem6  34112  constrfin  34136  locfinreflem  34230  zarcls  34264  ordtconnlem1  34314  fsumcvg4  34340  esumrnmpt2  34458  esumpinfval  34463  hasheuni  34475  measvuni  34604  eulerpartlemn  34771  elorvc  34850  ballotlemimin  34896  ballotlem7  34926  ballotth  34928  reprinrn  35005  reprpmtf1o  35013  reprdifc  35014  bnj1204  35400  bj-rabtrALT  37567  icorempo  37997  isbasisrelowllem1  38001  isbasisrelowllem2  38002  relowlssretop  38009  phpreu  38255  poimirlem26  38297  mbfposadd  38318  cover2  38366  aaitgo  43889  rababg  44300  nznngen  45026  permaxsep  45716  rfcnpre1  45739  rfcnpre2  45751  rabidim2  45820  rabidd  45873  disjf1o  45909  mptssid  45956  infnsuprnmpt  45965  allbutfiinf  46134  supminfxr2  46183  pimxrneun  46202  fsumsupp0  46294  limsupequzmpt2  46432  liminfequzmpt2  46505  cncfshift  46588  cncfperiod  46593  dvcosre  46626  dvnprodlem1  46660  itgsinexplem1  46668  stoweidlem27  46741  stoweidlem31  46745  stoweidlem34  46748  stoweidlem35  46749  stoweidlem59  46773  fourierdlem31  46852  etransclem32  46980  etransclem35  46983  etransclem37  46985  etransclem38  46986  sge0iunmptlemre  47129  meadjiunlem  47179  ovncvrrp  47278  hoidmv1lelem1  47305  hoidmvlelem2  47310  ovnhoilem2  47316  opnvonmbllem2  47347  ovolval4lem1  47363  preimagelt  47413  preimalegt  47414  pimconstlt1  47416  pimltpnff  47417  pimrecltpos  47422  pimgtmnff  47436  pimrecltneg  47438  smfaddlem1  47477  smflimlem2  47486  smfmullem4  47508  smflimsuplem4  47537  smflimsuplem7  47540