Theorem rabid 3095

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

Syntax hints:   ↔ wb 195   ∧ wa 383   ∈ wcel 1977  {crab 2900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-tru 1478  df-ex 1696  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-rab 2905

This theorem is referenced by:  rabeq2i  3170  reusv2lem4  4798  reusv2  4800  rabxfrd  4815  riotaxfrd  6541  tfis  6946  rankr1ai  8544  cfval2  8965  cflim3  8967  cflim2  8968  cfss  8970  cfslb  8971  cofsmo  8974  nnwos  11631  ramval  15550  ramub1lem1  15568  neiptopnei  20746  dissnlocfin  21142  hauseqlcld  21259  imasnopn  21303  imasncld  21304  imasncls  21305  ptcmplem4  21669  blval2  22177  psmetutop  22182  mbfinf  23238  itg2monolem1  23323  lhop1  23581  rusgranumwlkb0  26480  2spotmdisj  26595  numclwlk1lem2f  26619  rabrab  28722  rabexgfGS  28725  rabss3d  28736  fimarab  28825  aciunf1  28845  fpwrelmap  28896  locfinreflem  29235  ordtconlem1  29298  fsumcvg4  29324  esumrnmpt2  29457  esumpinfval  29462  hasheuni  29474  measvuni  29604  eulerpartlemn  29770  elorvc  29848  ballotlemimin  29894  ballotlem7  29924  ballotth  29926  bnj1204  30334  bj-rabtrALT  32119  icorempt2  32375  isbasisrelowllem1  32379  isbasisrelowllem2  32380  relowlssretop  32387  phpreu  32563  poimirlem26  32605  mbfposadd  32627  cover2  32678  aaitgo  36751  rababg  36898  nznngen  37537  rfcnpre1  38201  rfcnpre2  38213  rabid3  38285  rabidim2  38313  rabidim1  38318  disjf1o  38373  fsumsupp0  38645  cncfshift  38759  cncfperiod  38764  dvcosre  38799  dvnprodlem1  38836  itgsinexplem1  38845  stoweidlem27  38920  stoweidlem31  38924  stoweidlem34  38927  stoweidlem35  38928  stoweidlem59  38952  fourierdlem31  39031  etransclem32  39159  etransclem35  39162  etransclem37  39164  etransclem38  39165  rrxbasefi  39179  sge0iunmptlemre  39308  meadjiunlem  39358  ovncvrrp  39454  hoidmv1lelem1  39481  hoidmvlelem2  39486  ovnhoilem2  39492  opnvonmbllem2  39523  ovolval4lem1  39539  preimagelt  39589  preimalegt  39590  pimconstlt1  39592  pimltpnf  39593  pimrecltpos  39596  pimiooltgt  39598  preimageiingt  39607  preimaleiinlt  39608  pimrecltneg  39610  sssmf  39625  smfaddlem1  39649  smflimlem2  39658  smfmullem4  39679  rusgrnumwwlkb0  41174  av-numclwlk1lem2f  41522