Theorem rabid 3427

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  {crab 3405

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 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406

This theorem is referenced by:  rabidim1  3428  reqabi  3429  rabrab  3430  rabss3d  4044  eqrrabd  4049  reusv2lem4  5356  reusv2  5358  rabxfrd  5372  fimarab  6935  riotaxfrd  7378  tfis  7831  rankr1ai  9751  cfval2  10213  cflim3  10215  cflim2  10216  cfss  10218  cfslb  10219  cofsmo  10222  nnwos  12874  ramval  16979  ramub1lem1  16997  neiptopnei  23019  dissnlocfin  23416  hauseqlcld  23533  imasnopn  23577  imasncld  23578  imasncls  23579  ptcmplem4  23942  blval2  24450  psmetutop  24455  rrxbasefi  25310  mbfinf  25566  itg2monolem1  25651  lhop1  25919  ssltleft  27782  ssltright  27783  sltlpss  27819  cofcutr  27832  cofcutrtime  27835  addsproplem2  27877  rusgrnumwwlkb0  29901  difrab2  32427  aciunf1  32587  fpwrelmap  32656  cntrval2  33128  ply1mulrtss  33550  algextdeglem6  33712  constrfin  33736  locfinreflem  33830  zarcls  33864  ordtconnlem1  33914  fsumcvg4  33940  esumrnmpt2  34058  esumpinfval  34063  hasheuni  34075  measvuni  34204  eulerpartlemn  34372  elorvc  34451  ballotlemimin  34497  ballotlem7  34527  ballotth  34529  reprinrn  34609  reprpmtf1o  34617  reprdifc  34618  bnj1204  35002  bj-rabtrALT  36919  icorempo  37339  isbasisrelowllem1  37343  isbasisrelowllem2  37344  relowlssretop  37351  phpreu  37598  poimirlem26  37640  mbfposadd  37661  cover2  37709  aaitgo  43151  rababg  43563  nznngen  44305  permaxsep  44997  rfcnpre1  45013  rfcnpre2  45025  rabidim2  45096  rabidd  45149  disjf1o  45185  mptssid  45235  infnsuprnmpt  45244  allbutfiinf  45416  supminfxr2  45465  pimxrneun  45484  fsumsupp0  45576  limsupequzmpt2  45716  liminfequzmpt2  45789  cncfshift  45872  cncfperiod  45877  dvcosre  45910  dvnprodlem1  45944  itgsinexplem1  45952  stoweidlem27  46025  stoweidlem31  46029  stoweidlem34  46032  stoweidlem35  46033  stoweidlem59  46057  fourierdlem31  46136  etransclem32  46264  etransclem35  46267  etransclem37  46269  etransclem38  46270  sge0iunmptlemre  46413  meadjiunlem  46463  ovncvrrp  46562  hoidmv1lelem1  46589  hoidmvlelem2  46594  ovnhoilem2  46600  opnvonmbllem2  46631  ovolval4lem1  46647  preimagelt  46697  preimalegt  46698  pimconstlt1  46700  pimltpnff  46701  pimrecltpos  46706  pimiooltgt  46708  preimageiingt  46718  preimaleiinlt  46719  pimgtmnff  46720  pimrecltneg  46722  sssmf  46736  smfaddlem1  46761  smflimlem2  46770  smfmullem4  46792  smflimsuplem4  46821  smflimsuplem7  46824