Theorem rabid 3416

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2111  {crab 3395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396

This theorem is referenced by:  rabidim1  3417  reqabi  3418  rabrab  3419  rabss3d  4028  eqrrabd  4033  reusv2lem4  5337  reusv2  5339  rabxfrd  5353  fimarab  6896  riotaxfrd  7337  tfis  7785  rankr1ai  9691  cfval2  10151  cflim3  10153  cflim2  10154  cfss  10156  cfslb  10157  cofsmo  10160  nnwos  12813  ramval  16920  ramub1lem1  16938  neiptopnei  23047  dissnlocfin  23444  hauseqlcld  23561  imasnopn  23605  imasncld  23606  imasncls  23607  ptcmplem4  23970  blval2  24477  psmetutop  24482  rrxbasefi  25337  mbfinf  25593  itg2monolem1  25678  lhop1  25946  ssltleft  27815  ssltright  27816  sltlpss  27853  cofcutr  27868  cofcutrtime  27871  addsproplem2  27913  rusgrnumwwlkb0  29952  difrab2  32477  aciunf1  32645  fpwrelmap  32716  cntrval2  33140  ply1mulrtss  33545  algextdeglem6  33735  constrfin  33759  locfinreflem  33853  zarcls  33887  ordtconnlem1  33937  fsumcvg4  33963  esumrnmpt2  34081  esumpinfval  34086  hasheuni  34098  measvuni  34227  eulerpartlemn  34394  elorvc  34473  ballotlemimin  34519  ballotlem7  34549  ballotth  34551  reprinrn  34631  reprpmtf1o  34639  reprdifc  34640  bnj1204  35024  bj-rabtrALT  36975  icorempo  37395  isbasisrelowllem1  37399  isbasisrelowllem2  37400  relowlssretop  37407  phpreu  37654  poimirlem26  37696  mbfposadd  37717  cover2  37765  aaitgo  43265  rababg  43677  nznngen  44419  permaxsep  45110  rfcnpre1  45126  rfcnpre2  45138  rabidim2  45209  rabidd  45262  disjf1o  45298  mptssid  45348  infnsuprnmpt  45357  allbutfiinf  45528  supminfxr2  45577  pimxrneun  45596  fsumsupp0  45688  limsupequzmpt2  45826  liminfequzmpt2  45899  cncfshift  45982  cncfperiod  45987  dvcosre  46020  dvnprodlem1  46054  itgsinexplem1  46062  stoweidlem27  46135  stoweidlem31  46139  stoweidlem34  46142  stoweidlem35  46143  stoweidlem59  46167  fourierdlem31  46246  etransclem32  46374  etransclem35  46377  etransclem37  46379  etransclem38  46380  sge0iunmptlemre  46523  meadjiunlem  46573  ovncvrrp  46672  hoidmv1lelem1  46699  hoidmvlelem2  46704  ovnhoilem2  46710  opnvonmbllem2  46741  ovolval4lem1  46757  preimagelt  46807  preimalegt  46808  pimconstlt1  46810  pimltpnff  46811  pimrecltpos  46816  pimiooltgt  46818  preimageiingt  46828  preimaleiinlt  46829  pimgtmnff  46830  pimrecltneg  46832  sssmf  46846  smfaddlem1  46871  smflimlem2  46880  smfmullem4  46902  smflimsuplem4  46931  smflimsuplem7  46934