Theorem rabid 3310

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

Syntax hints:   ↔ wb 205   ∧ wa 396   ∈ wcel 2106  {crab 3068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073

This theorem is referenced by:  rabrab  3311  rabidim1  3312  rabeq2i  3422  reusv2lem4  5324  reusv2  5326  rabxfrd  5340  riotaxfrd  7267  tfis  7701  rankr1ai  9556  cfval2  10016  cflim3  10018  cflim2  10019  cfss  10021  cfslb  10022  cofsmo  10025  nnwos  12655  ramval  16709  ramub1lem1  16727  neiptopnei  22283  dissnlocfin  22680  hauseqlcld  22797  imasnopn  22841  imasncld  22842  imasncls  22843  ptcmplem4  23206  blval2  23718  psmetutop  23723  rrxbasefi  24574  mbfinf  24829  itg2monolem1  24915  lhop1  25178  rusgrnumwwlkb0  28336  difrab2  30845  eqrrabd  30849  rabss3d  30861  fimarab  30980  aciunf1  31000  fpwrelmap  31068  locfinreflem  31790  zarcls  31824  ordtconnlem1  31874  fsumcvg4  31900  esumrnmpt2  32036  esumpinfval  32041  hasheuni  32053  measvuni  32182  eulerpartlemn  32348  elorvc  32426  ballotlemimin  32472  ballotlem7  32502  ballotth  32504  reprinrn  32598  reprpmtf1o  32606  reprdifc  32607  bnj1204  32992  ssltleft  34054  ssltright  34055  sltlpss  34087  cofcutr  34092  cofcutrtime  34093  bj-rabtrALT  35119  icorempo  35522  isbasisrelowllem1  35526  isbasisrelowllem2  35527  relowlssretop  35534  phpreu  35761  poimirlem26  35803  mbfposadd  35824  cover2  35872  aaitgo  40987  rababg  41181  nznngen  41934  rfcnpre1  42562  rfcnpre2  42574  rabidim2  42652  disjf1o  42729  mptssid  42785  infnsuprnmpt  42796  allbutfiinf  42960  supminfxr2  43009  fsumsupp0  43119  limsupequzmpt2  43259  liminfequzmpt2  43332  cncfshift  43415  cncfperiod  43420  dvcosre  43453  dvnprodlem1  43487  itgsinexplem1  43495  stoweidlem27  43568  stoweidlem31  43572  stoweidlem34  43575  stoweidlem35  43576  stoweidlem59  43600  fourierdlem31  43679  etransclem32  43807  etransclem35  43810  etransclem37  43812  etransclem38  43813  sge0iunmptlemre  43953  meadjiunlem  44003  ovncvrrp  44102  hoidmv1lelem1  44129  hoidmvlelem2  44134  ovnhoilem2  44140  opnvonmbllem2  44171  ovolval4lem1  44187  preimagelt  44237  preimalegt  44238  pimconstlt1  44240  pimltpnf  44241  pimrecltpos  44245  pimiooltgt  44247  preimageiingt  44257  preimaleiinlt  44258  pimrecltneg  44260  sssmf  44274  smfaddlem1  44298  smflimlem2  44307  smfmullem4  44328  smflimsuplem4  44356  smflimsuplem7  44359