Theorem rabid 3452

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

Syntax hints:   ↔ wb 205   ∧ wa 396   ∈ wcel 2106  {crab 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433

This theorem is referenced by:  rabidim1  3453  reqabi  3454  rabrab  3455  rabss3d  4078  reusv2lem4  5398  reusv2  5400  rabxfrd  5414  riotaxfrd  7396  tfis  7840  rankr1ai  9789  cfval2  10251  cflim3  10253  cflim2  10254  cfss  10256  cfslb  10257  cofsmo  10260  nnwos  12895  ramval  16937  ramub1lem1  16955  neiptopnei  22627  dissnlocfin  23024  hauseqlcld  23141  imasnopn  23185  imasncld  23186  imasncls  23187  ptcmplem4  23550  blval2  24062  psmetutop  24067  rrxbasefi  24918  mbfinf  25173  itg2monolem1  25259  lhop1  25522  ssltleft  27354  ssltright  27355  sltlpss  27390  cofcutr  27400  cofcutrtime  27403  addsproplem2  27443  rusgrnumwwlkb0  29214  difrab2  31725  eqrrabd  31728  fimarab  31855  aciunf1  31875  fpwrelmap  31945  locfinreflem  32808  zarcls  32842  ordtconnlem1  32892  fsumcvg4  32918  esumrnmpt2  33054  esumpinfval  33059  hasheuni  33071  measvuni  33200  eulerpartlemn  33368  elorvc  33446  ballotlemimin  33492  ballotlem7  33522  ballotth  33524  reprinrn  33618  reprpmtf1o  33626  reprdifc  33627  bnj1204  34011  bj-rabtrALT  35799  icorempo  36220  isbasisrelowllem1  36224  isbasisrelowllem2  36225  relowlssretop  36232  phpreu  36460  poimirlem26  36502  mbfposadd  36523  cover2  36571  aaitgo  41889  rababg  42310  nznngen  43060  rfcnpre1  43688  rfcnpre2  43700  rabidim2  43776  rabidd  43834  disjf1o  43874  mptssid  43929  infnsuprnmpt  43940  allbutfiinf  44116  supminfxr2  44165  pimxrneun  44185  fsumsupp0  44280  limsupequzmpt2  44420  liminfequzmpt2  44493  cncfshift  44576  cncfperiod  44581  dvcosre  44614  dvnprodlem1  44648  itgsinexplem1  44656  stoweidlem27  44729  stoweidlem31  44733  stoweidlem34  44736  stoweidlem35  44737  stoweidlem59  44761  fourierdlem31  44840  etransclem32  44968  etransclem35  44971  etransclem37  44973  etransclem38  44974  sge0iunmptlemre  45117  meadjiunlem  45167  ovncvrrp  45266  hoidmv1lelem1  45293  hoidmvlelem2  45298  ovnhoilem2  45304  opnvonmbllem2  45335  ovolval4lem1  45351  preimagelt  45401  preimalegt  45402  pimconstlt1  45404  pimltpnff  45405  pimrecltpos  45410  pimiooltgt  45412  preimageiingt  45422  preimaleiinlt  45423  pimgtmnff  45424  pimrecltneg  45426  sssmf  45440  smfaddlem1  45465  smflimlem2  45474  smfmullem4  45496  smflimsuplem4  45525  smflimsuplem7  45528