Theorem rabid 3433

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  {crab 3413

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414

This theorem is used by:  rabidim1  3434  reqabi  3435  rabrab  3436  rabss3d  4029  eqrrabd  4034  reusv2lem4  5363  reusv2  5365  rabxfrd  5379  fimarab  6959  riotaxfrd  7411  tfis  7866  rankr1ai  9806  cfval2  10338  cflim3  10340  cflim2  10341  cfss  10343  cfslb  10344  cofsmo  10347  nnwos  13042  ramval  17186  ramub1lem1  17204  rspsn0  21526  neiptopnei  23450  dissnlocfin  23848  hauseqlcld  23965  imasnopn  24009  imasncld  24010  imasncls  24011  ptcmplem4  24374  blval2  24881  psmetutop  24886  rrxbasefi  25731  mbfinf  25986  itg2monolem1  26071  lhop1  26334  sltsleft  28246  sltsright  28247  ltslpss  28294  cofcutr  28310  cofcutrtime  28313  addsproplem2  28356  rusgrnumwwlkb0  30563  difrab2  33094  aciunf1  33257  fpwrelmap  33325  cntrval2  33732  ply1mulrtss  34114  algextdeglem6  34354  constrfin  34378  locfinreflem  34472  zarcls  34506  ordtconnlem1  34556  fsumcvg4  34582  esumrnmpt2  34700  esumpinfval  34705  hasheuni  34717  measvuni  34847  eulerpartlemn  35013  elorvc  35092  ballotlemimin  35138  ballotlem7  35168  ballotth  35170  reprinrn  35247  reprpmtf1o  35255  reprdifc  35256  bnj1204  35642  bj-rabtrALT  37844  icorempo  38274  isbasisrelowllem1  38278  isbasisrelowllem2  38279  relowlssretop  38286  phpreu  38527  poimirlem26  38564  mbfposadd  38585  cover2  38649  aaitgo  44163  rababg  44574  nznngen  45299  permaxsep  45996  rfcnpre1  46035  rfcnpre2  46047  rabidim2  46116  rabidd  46169  disjf1o  46205  mptssid  46252  infnsuprnmpt  46261  allbutfiinf  46429  supminfxr2  46478  pimxrneun  46497  fsumsupp0  46589  limsupequzmpt2  46727  liminfequzmpt2  46800  cncfshift  46883  cncfperiod  46888  dvcosre  46921  dvnprodlem1  46955  itgsinexplem1  46963  stoweidlem27  47036  stoweidlem31  47040  stoweidlem34  47043  stoweidlem35  47044  stoweidlem59  47068  fourierdlem31  47147  etransclem32  47275  etransclem35  47278  etransclem37  47280  etransclem38  47281  sge0iunmptlemre  47424  meadjiunlem  47474  ovncvrrp  47573  hoidmv1lelem1  47600  hoidmvlelem2  47605  ovnhoilem2  47611  opnvonmbllem2  47642  ovolval4lem1  47658  preimagelt  47708  preimalegt  47709  pimconstlt1  47711  pimltpnff  47712  pimrecltpos  47717  pimgtmnff  47731  pimrecltneg  47733  smfaddlem1  47772  smflimlem2  47781  smfmullem4  47803  smflimsuplem4  47832  smflimsuplem7  47835