Theorem rabid 3439

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

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

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 2148  ax-9 2156  ax-12 2216  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419

This theorem is used by:  rabidim1  3440  reqabi  3441  rabrab  3442  rabss3d  4036  eqrrabd  4041  reusv2lem4  5374  reusv2  5376  rabxfrd  5390  fimarab  6959  riotaxfrd  7410  tfis  7857  rankr1ai  9777  cfval2  10259  cflim3  10261  cflim2  10262  cfss  10264  cfslb  10265  cofsmo  10268  nnwos  12955  ramval  17090  ramub1lem1  17108  rspsn0  21422  neiptopnei  23339  dissnlocfin  23737  hauseqlcld  23854  imasnopn  23898  imasncld  23899  imasncls  23900  ptcmplem4  24263  blval2  24770  psmetutop  24775  rrxbasefi  25620  mbfinf  25875  itg2monolem1  25960  lhop1  26224  sltsleft  28104  sltsright  28105  ltslpss  28152  cofcutr  28168  cofcutrtime  28171  addsproplem2  28214  rusgrnumwwlkb0  30390  difrab2  32915  aciunf1  33079  fpwrelmap  33148  cntrval2  33555  ply1mulrtss  33936  algextdeglem6  34176  constrfin  34200  locfinreflem  34294  zarcls  34328  ordtconnlem1  34378  fsumcvg4  34404  esumrnmpt2  34522  esumpinfval  34527  hasheuni  34539  measvuni  34669  eulerpartlemn  34836  elorvc  34915  ballotlemimin  34961  ballotlem7  34991  ballotth  34993  reprinrn  35070  reprpmtf1o  35078  reprdifc  35079  bnj1204  35465  bj-rabtrALT  37624  icorempo  38054  isbasisrelowllem1  38058  isbasisrelowllem2  38059  relowlssretop  38066  phpreu  38312  poimirlem26  38354  mbfposadd  38375  cover2  38424  aaitgo  43947  rababg  44358  nznngen  45084  permaxsep  45774  rfcnpre1  45797  rfcnpre2  45809  rabidim2  45878  rabidd  45931  disjf1o  45967  mptssid  46014  infnsuprnmpt  46023  allbutfiinf  46192  supminfxr2  46241  pimxrneun  46260  fsumsupp0  46352  limsupequzmpt2  46490  liminfequzmpt2  46563  cncfshift  46646  cncfperiod  46651  dvcosre  46684  dvnprodlem1  46718  itgsinexplem1  46726  stoweidlem27  46799  stoweidlem31  46803  stoweidlem34  46806  stoweidlem35  46807  stoweidlem59  46831  fourierdlem31  46910  etransclem32  47038  etransclem35  47041  etransclem37  47043  etransclem38  47044  sge0iunmptlemre  47187  meadjiunlem  47237  ovncvrrp  47336  hoidmv1lelem1  47363  hoidmvlelem2  47368  ovnhoilem2  47374  opnvonmbllem2  47405  ovolval4lem1  47421  preimagelt  47471  preimalegt  47472  pimconstlt1  47474  pimltpnff  47475  pimrecltpos  47480  pimgtmnff  47494  pimrecltneg  47496  smfaddlem1  47535  smflimlem2  47544  smfmullem4  47566  smflimsuplem4  47595  smflimsuplem7  47598