Theorem rabid 3412

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

Syntax hints:   ↔ wb 207   ∧ wa 396   ∈ wcel 2119  {crab 3391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392

This theorem is referenced by:  rabidim1  3413  reqabi  3414  rabrab  3415  rabss3d  4012  eqrrabd  4017  reusv2lem4  5330  reusv2  5332  rabxfrd  5346  fimarab  6901  riotaxfrd  7347  tfis  7795  rankr1ai  9713  cfval2  10173  cflim3  10175  cflim2  10176  cfss  10178  cfslb  10179  cofsmo  10182  nnwos  12856  ramval  16970  ramub1lem1  16988  neiptopnei  23115  dissnlocfin  23512  hauseqlcld  23629  imasnopn  23673  imasncld  23674  imasncls  23675  ptcmplem4  24038  blval2  24545  psmetutop  24550  rrxbasefi  25395  mbfinf  25650  itg2monolem1  25735  lhop1  25999  sltsleft  27870  sltsright  27871  ltslpss  27918  cofcutr  27934  cofcutrtime  27937  addsproplem2  27980  rusgrnumwwlkb0  30060  difrab2  32585  aciunf1  32755  fpwrelmap  32825  cntrval2  33252  ply1mulrtss  33665  algextdeglem6  33906  constrfin  33930  locfinreflem  34024  zarcls  34058  ordtconnlem1  34108  fsumcvg4  34134  esumrnmpt2  34252  esumpinfval  34257  hasheuni  34269  measvuni  34398  eulerpartlemn  34565  elorvc  34644  ballotlemimin  34690  ballotlem7  34720  ballotth  34722  reprinrn  34802  reprpmtf1o  34810  reprdifc  34811  bnj1204  35194  bj-rabtrALT  37284  icorempo  37713  isbasisrelowllem1  37717  isbasisrelowllem2  37718  relowlssretop  37725  phpreu  37971  poimirlem26  38013  mbfposadd  38034  cover2  38082  aaitgo  43607  rababg  44018  nznngen  44760  permaxsep  45451  rfcnpre1  45467  rfcnpre2  45479  rabidim2  45549  rabidd  45602  disjf1o  45638  mptssid  45685  infnsuprnmpt  45694  allbutfiinf  45863  supminfxr2  45912  pimxrneun  45931  fsumsupp0  46023  limsupequzmpt2  46161  liminfequzmpt2  46234  cncfshift  46317  cncfperiod  46322  dvcosre  46355  dvnprodlem1  46389  itgsinexplem1  46397  stoweidlem27  46470  stoweidlem31  46474  stoweidlem34  46477  stoweidlem35  46478  stoweidlem59  46502  fourierdlem31  46581  etransclem32  46709  etransclem35  46712  etransclem37  46714  etransclem38  46715  sge0iunmptlemre  46858  meadjiunlem  46908  ovncvrrp  47007  hoidmv1lelem1  47034  hoidmvlelem2  47039  ovnhoilem2  47045  opnvonmbllem2  47076  ovolval4lem1  47092  preimagelt  47142  preimalegt  47143  pimconstlt1  47145  pimltpnff  47146  pimrecltpos  47151  pimgtmnff  47165  pimrecltneg  47167  sssmf  47181  smfaddlem1  47206  smflimlem2  47215  smfmullem4  47237  smflimsuplem4  47266  smflimsuplem7  47269