Theorem rabid 3436

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417

This theorem is used by:  rabidim1  3437  reqabi  3438  rabrab  3439  rabss3d  4009  eqrrabd  4014  reusv2lem4  5370  reusv2  5372  rabxfrd  5386  fimarab  6990  riotaxfrd  7442  tfis  7900  rankr1ai  9843  cfval2  10377  cflim3  10379  cflim2  10380  cfss  10382  cfslb  10383  cofsmo  10386  nnwos  13082  ramval  17230  ramub1lem1  17248  rspsn0  21577  neiptopnei  23505  dissnlocfin  23903  hauseqlcld  24020  imasnopn  24064  imasncld  24065  imasncls  24066  ptcmplem4  24429  blval2  24936  psmetutop  24941  rrxbasefi  25786  mbfinf  26041  itg2monolem1  26126  lhop1  26389  sltsleft  28303  sltsright  28304  ltslpss  28351  cofcutr  28367  cofcutrtime  28370  addsproplem2  28413  rusgrnumwwlkb0  30620  difrab2  33193  aciunf1  33355  fpwrelmap  33421  cntrval2  33831  ply1mulrtss  34217  algextdeglem6  34465  constrfin  34489  locfinreflem  34583  zarcls  34617  ordtconnlem1  34667  fsumcvg4  34693  esumrnmpt2  34811  esumpinfval  34816  hasheuni  34828  measvuni  34958  eulerpartlemn  35124  elorvc  35203  ballotlemimin  35249  ballotlem7  35279  ballotth  35281  reprinrn  35358  reprpmtf1o  35366  reprdifc  35367  bnj1204  35753  bj-rabtrALT  38059  icorempo  38542  isbasisrelowllem1  38546  isbasisrelowllem2  38547  relowlssretop  38554  phpreu  38795  poimirlem26  38832  mbfposadd  38853  cover2  38917  aaitgo  44429  rababg  44836  nznngen  45561  permaxsep  46261  rfcnpre1  46310  rfcnpre2  46322  rabidim2  46390  rabidd  46443  disjf1o  46479  mptssid  46526  infnsuprnmpt  46535  allbutfiinf  46703  supminfxr2  46752  pimxrneun  46771  fsumsupp0  46863  limsupequzmpt2  47001  liminfequzmpt2  47074  cncfshift  47157  cncfperiod  47162  dvcosre  47195  dvnprodlem1  47229  itgsinexplem1  47237  stoweidlem27  47310  stoweidlem31  47314  stoweidlem34  47317  stoweidlem35  47318  stoweidlem59  47342  fourierdlem31  47421  etransclem32  47549  etransclem35  47552  etransclem37  47554  etransclem38  47555  sge0iunmptlemre  47698  meadjiunlem  47748  ovncvrrp  47847  hoidmv1lelem1  47874  hoidmvlelem2  47879  ovnhoilem2  47885  opnvonmbllem2  47916  ovolval4lem1  47932  preimagelt  47982  preimalegt  47983  pimconstlt1  47985  pimltpnff  47986  pimrecltpos  47991  pimgtmnff  48005  pimrecltneg  48007  smfaddlem1  48046  smflimlem2  48055  smfmullem4  48077  smflimsuplem4  48106  smflimsuplem7  48109