Theorem rabid 3458

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  {crab 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437

This theorem is referenced by:  rabidim1  3459  reqabi  3460  rabrab  3461  rabss3d  4081  eqrrabd  4086  reusv2lem4  5401  reusv2  5403  rabxfrd  5417  fimarab  6983  riotaxfrd  7422  tfis  7876  rankr1ai  9838  cfval2  10300  cflim3  10302  cflim2  10303  cfss  10305  cfslb  10306  cofsmo  10309  nnwos  12957  ramval  17046  ramub1lem1  17064  neiptopnei  23140  dissnlocfin  23537  hauseqlcld  23654  imasnopn  23698  imasncld  23699  imasncls  23700  ptcmplem4  24063  blval2  24575  psmetutop  24580  rrxbasefi  25444  mbfinf  25700  itg2monolem1  25785  lhop1  26053  ssltleft  27909  ssltright  27910  sltlpss  27945  cofcutr  27958  cofcutrtime  27961  addsproplem2  28003  rusgrnumwwlkb0  29991  difrab2  32517  aciunf1  32673  fpwrelmap  32744  ply1mulrtss  33606  algextdeglem6  33763  constrfin  33787  locfinreflem  33839  zarcls  33873  ordtconnlem1  33923  fsumcvg4  33949  esumrnmpt2  34069  esumpinfval  34074  hasheuni  34086  measvuni  34215  eulerpartlemn  34383  elorvc  34462  ballotlemimin  34508  ballotlem7  34538  ballotth  34540  reprinrn  34633  reprpmtf1o  34641  reprdifc  34642  bnj1204  35026  bj-rabtrALT  36932  icorempo  37352  isbasisrelowllem1  37356  isbasisrelowllem2  37357  relowlssretop  37364  phpreu  37611  poimirlem26  37653  mbfposadd  37674  cover2  37722  aaitgo  43174  rababg  43587  nznngen  44335  rfcnpre1  45024  rfcnpre2  45036  rabidim2  45107  rabidd  45160  disjf1o  45196  mptssid  45247  infnsuprnmpt  45257  allbutfiinf  45431  supminfxr2  45480  pimxrneun  45499  fsumsupp0  45593  limsupequzmpt2  45733  liminfequzmpt2  45806  cncfshift  45889  cncfperiod  45894  dvcosre  45927  dvnprodlem1  45961  itgsinexplem1  45969  stoweidlem27  46042  stoweidlem31  46046  stoweidlem34  46049  stoweidlem35  46050  stoweidlem59  46074  fourierdlem31  46153  etransclem32  46281  etransclem35  46284  etransclem37  46286  etransclem38  46287  sge0iunmptlemre  46430  meadjiunlem  46480  ovncvrrp  46579  hoidmv1lelem1  46606  hoidmvlelem2  46611  ovnhoilem2  46617  opnvonmbllem2  46648  ovolval4lem1  46664  preimagelt  46714  preimalegt  46715  pimconstlt1  46717  pimltpnff  46718  pimrecltpos  46723  pimiooltgt  46725  preimageiingt  46735  preimaleiinlt  46736  pimgtmnff  46737  pimrecltneg  46739  sssmf  46753  smfaddlem1  46778  smflimlem2  46787  smfmullem4  46809  smflimsuplem4  46838  smflimsuplem7  46841