Theorem rabid 3432

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413

This theorem is used by:  rabidim1  3433  reqabi  3434  rabrab  3435  rabss3d  4005  eqrrabd  4010  reusv2lem4  5363  reusv2  5365  rabxfrd  5379  fimarab  6964  riotaxfrd  7415  tfis  7870  rankr1ai  9813  cfval2  10345  cflim3  10347  cflim2  10348  cfss  10350  cfslb  10351  cofsmo  10354  nnwos  13049  ramval  17195  ramub1lem1  17213  rspsn0  21535  neiptopnei  23459  dissnlocfin  23857  hauseqlcld  23974  imasnopn  24018  imasncld  24019  imasncls  24020  ptcmplem4  24383  blval2  24890  psmetutop  24895  rrxbasefi  25740  mbfinf  25995  itg2monolem1  26080  lhop1  26343  sltsleft  28255  sltsright  28256  ltslpss  28303  cofcutr  28319  cofcutrtime  28322  addsproplem2  28365  rusgrnumwwlkb0  30572  difrab2  33145  aciunf1  33308  fpwrelmap  33375  cntrval2  33782  ply1mulrtss  34164  algextdeglem6  34404  constrfin  34428  locfinreflem  34522  zarcls  34556  ordtconnlem1  34606  fsumcvg4  34632  esumrnmpt2  34750  esumpinfval  34755  hasheuni  34767  measvuni  34897  eulerpartlemn  35063  elorvc  35142  ballotlemimin  35188  ballotlem7  35218  ballotth  35220  reprinrn  35297  reprpmtf1o  35305  reprdifc  35306  bnj1204  35692  bj-rabtrALT  37968  icorempo  38411  isbasisrelowllem1  38415  isbasisrelowllem2  38416  relowlssretop  38423  phpreu  38664  poimirlem26  38701  mbfposadd  38722  cover2  38786  aaitgo  44301  rababg  44712  nznngen  45437  permaxsep  46133  rfcnpre1  46172  rfcnpre2  46184  rabidim2  46253  rabidd  46306  disjf1o  46342  mptssid  46389  infnsuprnmpt  46398  allbutfiinf  46566  supminfxr2  46615  pimxrneun  46634  fsumsupp0  46726  limsupequzmpt2  46864  liminfequzmpt2  46937  cncfshift  47020  cncfperiod  47025  dvcosre  47058  dvnprodlem1  47092  itgsinexplem1  47100  stoweidlem27  47173  stoweidlem31  47177  stoweidlem34  47180  stoweidlem35  47181  stoweidlem59  47205  fourierdlem31  47284  etransclem32  47412  etransclem35  47415  etransclem37  47417  etransclem38  47418  sge0iunmptlemre  47561  meadjiunlem  47611  ovncvrrp  47710  hoidmv1lelem1  47737  hoidmvlelem2  47742  ovnhoilem2  47748  opnvonmbllem2  47779  ovolval4lem1  47795  preimagelt  47845  preimalegt  47846  pimconstlt1  47848  pimltpnff  47849  pimrecltpos  47854  pimgtmnff  47868  pimrecltneg  47870  smfaddlem1  47909  smflimlem2  47918  smfmullem4  47940  smflimsuplem4  47969  smflimsuplem7  47972