Theorem rabid 3304

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

Syntax hints:   ↔ wb 205   ∧ wa 395   ∈ wcel 2108  {crab 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072

This theorem is referenced by:  rabrab  3305  rabidim1  3306  rabeq2i  3412  reusv2lem4  5319  reusv2  5321  rabxfrd  5335  riotaxfrd  7247  tfis  7676  rankr1ai  9487  cfval2  9947  cflim3  9949  cflim2  9950  cfss  9952  cfslb  9953  cofsmo  9956  nnwos  12584  ramval  16637  ramub1lem1  16655  neiptopnei  22191  dissnlocfin  22588  hauseqlcld  22705  imasnopn  22749  imasncld  22750  imasncls  22751  ptcmplem4  23114  blval2  23624  psmetutop  23629  rrxbasefi  24479  mbfinf  24734  itg2monolem1  24820  lhop1  25083  rusgrnumwwlkb0  28237  difrab2  30746  eqrrabd  30750  rabss3d  30762  fimarab  30881  aciunf1  30902  fpwrelmap  30970  locfinreflem  31692  zarcls  31726  ordtconnlem1  31776  fsumcvg4  31802  esumrnmpt2  31936  esumpinfval  31941  hasheuni  31953  measvuni  32082  eulerpartlemn  32248  elorvc  32326  ballotlemimin  32372  ballotlem7  32402  ballotth  32404  reprinrn  32498  reprpmtf1o  32506  reprdifc  32507  bnj1204  32892  ssltleft  33981  ssltright  33982  sltlpss  34014  cofcutr  34019  cofcutrtime  34020  bj-rabtrALT  35046  icorempo  35449  isbasisrelowllem1  35453  isbasisrelowllem2  35454  relowlssretop  35461  phpreu  35688  poimirlem26  35730  mbfposadd  35751  cover2  35799  aaitgo  40903  rababg  41070  nznngen  41823  rfcnpre1  42451  rfcnpre2  42463  rabidim2  42541  disjf1o  42618  mptssid  42674  infnsuprnmpt  42685  allbutfiinf  42850  supminfxr2  42899  fsumsupp0  43009  limsupequzmpt2  43149  liminfequzmpt2  43222  cncfshift  43305  cncfperiod  43310  dvcosre  43343  dvnprodlem1  43377  itgsinexplem1  43385  stoweidlem27  43458  stoweidlem31  43462  stoweidlem34  43465  stoweidlem35  43466  stoweidlem59  43490  fourierdlem31  43569  etransclem32  43697  etransclem35  43700  etransclem37  43702  etransclem38  43703  sge0iunmptlemre  43843  meadjiunlem  43893  ovncvrrp  43992  hoidmv1lelem1  44019  hoidmvlelem2  44024  ovnhoilem2  44030  opnvonmbllem2  44061  ovolval4lem1  44077  preimagelt  44126  preimalegt  44127  pimconstlt1  44129  pimltpnf  44130  pimrecltpos  44133  pimiooltgt  44135  preimageiingt  44144  preimaleiinlt  44145  pimrecltneg  44147  sssmf  44161  smfaddlem1  44185  smflimlem2  44194  smfmullem4  44215  smflimsuplem4  44243  smflimsuplem7  44246