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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  {crab 3394

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 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395

This theorem is referenced by:  rabidim1  3417  reqabi  3418  rabrab  3419  rabss3d  4032  eqrrabd  4037  reusv2lem4  5340  reusv2  5342  rabxfrd  5356  fimarab  6897  riotaxfrd  7340  tfis  7788  rankr1ai  9694  cfval2  10154  cflim3  10156  cflim2  10157  cfss  10159  cfslb  10160  cofsmo  10163  nnwos  12816  ramval  16920  ramub1lem1  16938  neiptopnei  23017  dissnlocfin  23414  hauseqlcld  23531  imasnopn  23575  imasncld  23576  imasncls  23577  ptcmplem4  23940  blval2  24448  psmetutop  24453  rrxbasefi  25308  mbfinf  25564  itg2monolem1  25649  lhop1  25917  ssltleft  27784  ssltright  27785  sltlpss  27822  cofcutr  27837  cofcutrtime  27840  addsproplem2  27882  rusgrnumwwlkb0  29916  difrab2  32442  aciunf1  32606  fpwrelmap  32676  cntrval2  33113  ply1mulrtss  33517  algextdeglem6  33689  constrfin  33713  locfinreflem  33807  zarcls  33841  ordtconnlem1  33891  fsumcvg4  33917  esumrnmpt2  34035  esumpinfval  34040  hasheuni  34052  measvuni  34181  eulerpartlemn  34349  elorvc  34428  ballotlemimin  34474  ballotlem7  34504  ballotth  34506  reprinrn  34586  reprpmtf1o  34594  reprdifc  34595  bnj1204  34979  bj-rabtrALT  36905  icorempo  37325  isbasisrelowllem1  37329  isbasisrelowllem2  37330  relowlssretop  37337  phpreu  37584  poimirlem26  37626  mbfposadd  37647  cover2  37695  aaitgo  43135  rababg  43547  nznngen  44289  permaxsep  44981  rfcnpre1  44997  rfcnpre2  45009  rabidim2  45080  rabidd  45133  disjf1o  45169  mptssid  45219  infnsuprnmpt  45228  allbutfiinf  45399  supminfxr2  45448  pimxrneun  45467  fsumsupp0  45559  limsupequzmpt2  45699  liminfequzmpt2  45772  cncfshift  45855  cncfperiod  45860  dvcosre  45893  dvnprodlem1  45927  itgsinexplem1  45935  stoweidlem27  46008  stoweidlem31  46012  stoweidlem34  46015  stoweidlem35  46016  stoweidlem59  46040  fourierdlem31  46119  etransclem32  46247  etransclem35  46250  etransclem37  46252  etransclem38  46253  sge0iunmptlemre  46396  meadjiunlem  46446  ovncvrrp  46545  hoidmv1lelem1  46572  hoidmvlelem2  46577  ovnhoilem2  46583  opnvonmbllem2  46614  ovolval4lem1  46630  preimagelt  46680  preimalegt  46681  pimconstlt1  46683  pimltpnff  46684  pimrecltpos  46689  pimiooltgt  46691  preimageiingt  46701  preimaleiinlt  46702  pimgtmnff  46703  pimrecltneg  46705  sssmf  46719  smfaddlem1  46744  smflimlem2  46753  smfmullem4  46775  smflimsuplem4  46804  smflimsuplem7  46807