Theorem rabid 3327

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

Syntax hints:   ↔ wb 198   ∧ wa 386   ∈ wcel 2166  {crab 3122

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-12 2222  ax-ext 2804

This theorem depends on definitions:  df-bi 199  df-an 387  df-tru 1662  df-ex 1881  df-sb 2070  df-clab 2813  df-cleq 2819  df-clel 2822  df-rab 3127

This theorem is referenced by:  rabrab  3328  rabidim1  3329  rabeq2i  3411  reusv2lem4  5102  reusv2  5104  rabxfrd  5118  riotaxfrd  6898  tfis  7316  rankr1ai  8939  cfval2  9398  cflim3  9400  cflim2  9401  cfss  9403  cfslb  9404  cofsmo  9407  nnwos  12039  ramval  16084  ramub1lem1  16102  neiptopnei  21308  dissnlocfin  21704  hauseqlcld  21821  imasnopn  21865  imasncld  21866  imasncls  21867  ptcmplem4  22230  blval2  22738  psmetutop  22743  rrxbasefi  23579  mbfinf  23832  itg2monolem1  23917  lhop1  24177  rusgrnumwwlkb0  27301  difrab2  29888  rabexgfGS  29889  rabss3d  29900  fimarab  29995  aciunf1  30013  fpwrelmap  30057  locfinreflem  30453  ordtconnlem1  30516  fsumcvg4  30542  esumrnmpt2  30676  esumpinfval  30681  hasheuni  30693  measvuni  30823  eulerpartlemn  30989  elorvc  31068  ballotlemimin  31114  ballotlem7  31144  ballotth  31146  reprinrn  31246  reprpmtf1o  31254  reprdifc  31255  bnj1204  31627  bj-rabtrALT  33452  icorempt2  33745  isbasisrelowllem1  33749  isbasisrelowllem2  33750  relowlssretop  33757  phpreu  33937  poimirlem26  33980  mbfposadd  34001  cover2  34052  aaitgo  38576  rababg  38721  nznngen  39356  rfcnpre1  39997  rfcnpre2  40009  rabidim2  40101  disjf1o  40187  mptssid  40252  infnsuprnmpt  40266  allbutfiinf  40443  supminfxr2  40494  fsumsupp0  40606  limsupequzmpt2  40746  liminfequzmpt2  40819  cncfshift  40883  cncfperiod  40888  dvcosre  40922  dvnprodlem1  40957  itgsinexplem1  40965  stoweidlem27  41039  stoweidlem31  41043  stoweidlem34  41046  stoweidlem35  41047  stoweidlem59  41071  fourierdlem31  41150  etransclem32  41278  etransclem35  41281  etransclem37  41283  etransclem38  41284  sge0iunmptlemre  41424  meadjiunlem  41474  ovncvrrp  41573  hoidmv1lelem1  41600  hoidmvlelem2  41605  ovnhoilem2  41611  opnvonmbllem2  41642  ovolval4lem1  41658  preimagelt  41707  preimalegt  41708  pimconstlt1  41710  pimltpnf  41711  pimrecltpos  41714  pimiooltgt  41716  preimageiingt  41725  preimaleiinlt  41726  pimrecltneg  41728  sssmf  41742  smfaddlem1  41766  smflimlem2  41775  smfmullem4  41796  smflimsuplem4  41824  smflimsuplem7  41827