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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  {crab 3415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-12 2177  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416

This theorem is referenced by:  rabidim1  3438  reqabi  3439  rabrab  3440  rabss3d  4056  eqrrabd  4061  reusv2lem4  5371  reusv2  5373  rabxfrd  5387  fimarab  6952  riotaxfrd  7394  tfis  7848  rankr1ai  9810  cfval2  10272  cflim3  10274  cflim2  10275  cfss  10277  cfslb  10278  cofsmo  10281  nnwos  12929  ramval  17026  ramub1lem1  17044  neiptopnei  23068  dissnlocfin  23465  hauseqlcld  23582  imasnopn  23626  imasncld  23627  imasncls  23628  ptcmplem4  23991  blval2  24499  psmetutop  24504  rrxbasefi  25360  mbfinf  25616  itg2monolem1  25701  lhop1  25969  ssltleft  27826  ssltright  27827  sltlpss  27862  cofcutr  27875  cofcutrtime  27878  addsproplem2  27920  rusgrnumwwlkb0  29899  difrab2  32425  aciunf1  32587  fpwrelmap  32656  ply1mulrtss  33540  algextdeglem6  33702  constrfin  33726  locfinreflem  33817  zarcls  33851  ordtconnlem1  33901  fsumcvg4  33927  esumrnmpt2  34045  esumpinfval  34050  hasheuni  34062  measvuni  34191  eulerpartlemn  34359  elorvc  34438  ballotlemimin  34484  ballotlem7  34514  ballotth  34516  reprinrn  34596  reprpmtf1o  34604  reprdifc  34605  bnj1204  34989  bj-rabtrALT  36895  icorempo  37315  isbasisrelowllem1  37319  isbasisrelowllem2  37320  relowlssretop  37327  phpreu  37574  poimirlem26  37616  mbfposadd  37637  cover2  37685  aaitgo  43133  rababg  43545  nznngen  44288  permaxsep  44980  rfcnpre1  44991  rfcnpre2  45003  rabidim2  45074  rabidd  45127  disjf1o  45163  mptssid  45213  infnsuprnmpt  45222  allbutfiinf  45395  supminfxr2  45444  pimxrneun  45463  fsumsupp0  45555  limsupequzmpt2  45695  liminfequzmpt2  45768  cncfshift  45851  cncfperiod  45856  dvcosre  45889  dvnprodlem1  45923  itgsinexplem1  45931  stoweidlem27  46004  stoweidlem31  46008  stoweidlem34  46011  stoweidlem35  46012  stoweidlem59  46036  fourierdlem31  46115  etransclem32  46243  etransclem35  46246  etransclem37  46248  etransclem38  46249  sge0iunmptlemre  46392  meadjiunlem  46442  ovncvrrp  46541  hoidmv1lelem1  46568  hoidmvlelem2  46573  ovnhoilem2  46579  opnvonmbllem2  46610  ovolval4lem1  46626  preimagelt  46676  preimalegt  46677  pimconstlt1  46679  pimltpnff  46680  pimrecltpos  46685  pimiooltgt  46687  preimageiingt  46697  preimaleiinlt  46698  pimgtmnff  46699  pimrecltneg  46701  sssmf  46715  smfaddlem1  46740  smflimlem2  46749  smfmullem4  46771  smflimsuplem4  46800  smflimsuplem7  46803