Theorem rabid 3465

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444

This theorem is referenced by:  rabidim1  3466  reqabi  3467  rabrab  3468  rabss3d  4104  eqrrabd  4109  reusv2lem4  5419  reusv2  5421  rabxfrd  5435  fimarab  6996  riotaxfrd  7439  tfis  7892  rankr1ai  9867  cfval2  10329  cflim3  10331  cflim2  10332  cfss  10334  cfslb  10335  cofsmo  10338  nnwos  12980  ramval  17055  ramub1lem1  17073  neiptopnei  23161  dissnlocfin  23558  hauseqlcld  23675  imasnopn  23719  imasncld  23720  imasncls  23721  ptcmplem4  24084  blval2  24596  psmetutop  24601  rrxbasefi  25463  mbfinf  25719  itg2monolem1  25805  lhop1  26073  ssltleft  27927  ssltright  27928  sltlpss  27963  cofcutr  27976  cofcutrtime  27979  addsproplem2  28021  rusgrnumwwlkb0  30004  difrab2  32526  aciunf1  32681  fpwrelmap  32747  ply1mulrtss  33571  algextdeglem6  33713  constrfin  33736  locfinreflem  33786  zarcls  33820  ordtconnlem1  33870  fsumcvg4  33896  esumrnmpt2  34032  esumpinfval  34037  hasheuni  34049  measvuni  34178  eulerpartlemn  34346  elorvc  34424  ballotlemimin  34470  ballotlem7  34500  ballotth  34502  reprinrn  34595  reprpmtf1o  34603  reprdifc  34604  bnj1204  34988  bj-rabtrALT  36897  icorempo  37317  isbasisrelowllem1  37321  isbasisrelowllem2  37322  relowlssretop  37329  phpreu  37564  poimirlem26  37606  mbfposadd  37627  cover2  37675  aaitgo  43119  rababg  43536  nznngen  44285  rfcnpre1  44919  rfcnpre2  44931  rabidim2  45004  rabidd  45060  disjf1o  45098  mptssid  45149  infnsuprnmpt  45159  allbutfiinf  45335  supminfxr2  45384  pimxrneun  45404  fsumsupp0  45499  limsupequzmpt2  45639  liminfequzmpt2  45712  cncfshift  45795  cncfperiod  45800  dvcosre  45833  dvnprodlem1  45867  itgsinexplem1  45875  stoweidlem27  45948  stoweidlem31  45952  stoweidlem34  45955  stoweidlem35  45956  stoweidlem59  45980  fourierdlem31  46059  etransclem32  46187  etransclem35  46190  etransclem37  46192  etransclem38  46193  sge0iunmptlemre  46336  meadjiunlem  46386  ovncvrrp  46485  hoidmv1lelem1  46512  hoidmvlelem2  46517  ovnhoilem2  46523  opnvonmbllem2  46554  ovolval4lem1  46570  preimagelt  46620  preimalegt  46621  pimconstlt1  46623  pimltpnff  46624  pimrecltpos  46629  pimiooltgt  46631  preimageiingt  46641  preimaleiinlt  46642  pimgtmnff  46643  pimrecltneg  46645  sssmf  46659  smfaddlem1  46684  smflimlem2  46693  smfmullem4  46715  smflimsuplem4  46744  smflimsuplem7  46747