Theorem rabid 3424

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

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

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 3403

This theorem is referenced by:  rabidim1  3425  reqabi  3426  rabrab  3427  rabss3d  4040  eqrrabd  4045  reusv2lem4  5351  reusv2  5353  rabxfrd  5367  fimarab  6917  riotaxfrd  7360  tfis  7811  rankr1ai  9727  cfval2  10189  cflim3  10191  cflim2  10192  cfss  10194  cfslb  10195  cofsmo  10198  nnwos  12850  ramval  16955  ramub1lem1  16973  neiptopnei  23052  dissnlocfin  23449  hauseqlcld  23566  imasnopn  23610  imasncld  23611  imasncls  23612  ptcmplem4  23975  blval2  24483  psmetutop  24488  rrxbasefi  25343  mbfinf  25599  itg2monolem1  25684  lhop1  25952  ssltleft  27819  ssltright  27820  sltlpss  27857  cofcutr  27872  cofcutrtime  27875  addsproplem2  27917  rusgrnumwwlkb0  29951  difrab2  32477  aciunf1  32637  fpwrelmap  32706  cntrval2  33143  ply1mulrtss  33543  algextdeglem6  33705  constrfin  33729  locfinreflem  33823  zarcls  33857  ordtconnlem1  33907  fsumcvg4  33933  esumrnmpt2  34051  esumpinfval  34056  hasheuni  34068  measvuni  34197  eulerpartlemn  34365  elorvc  34444  ballotlemimin  34490  ballotlem7  34520  ballotth  34522  reprinrn  34602  reprpmtf1o  34610  reprdifc  34611  bnj1204  34995  bj-rabtrALT  36912  icorempo  37332  isbasisrelowllem1  37336  isbasisrelowllem2  37337  relowlssretop  37344  phpreu  37591  poimirlem26  37633  mbfposadd  37654  cover2  37702  aaitgo  43144  rababg  43556  nznngen  44298  permaxsep  44990  rfcnpre1  45006  rfcnpre2  45018  rabidim2  45089  rabidd  45142  disjf1o  45178  mptssid  45228  infnsuprnmpt  45237  allbutfiinf  45409  supminfxr2  45458  pimxrneun  45477  fsumsupp0  45569  limsupequzmpt2  45709  liminfequzmpt2  45782  cncfshift  45865  cncfperiod  45870  dvcosre  45903  dvnprodlem1  45937  itgsinexplem1  45945  stoweidlem27  46018  stoweidlem31  46022  stoweidlem34  46025  stoweidlem35  46026  stoweidlem59  46050  fourierdlem31  46129  etransclem32  46257  etransclem35  46260  etransclem37  46262  etransclem38  46263  sge0iunmptlemre  46406  meadjiunlem  46456  ovncvrrp  46555  hoidmv1lelem1  46582  hoidmvlelem2  46587  ovnhoilem2  46593  opnvonmbllem2  46624  ovolval4lem1  46640  preimagelt  46690  preimalegt  46691  pimconstlt1  46693  pimltpnff  46694  pimrecltpos  46699  pimiooltgt  46701  preimageiingt  46711  preimaleiinlt  46712  pimgtmnff  46713  pimrecltneg  46715  sssmf  46729  smfaddlem1  46754  smflimlem2  46763  smfmullem4  46785  smflimsuplem4  46814  smflimsuplem7  46817