Theorem rabid 3410

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  {crab 3389

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390

This theorem is referenced by:  rabidim1  3411  reqabi  3412  rabrab  3413  rabss3d  4021  eqrrabd  4026  reusv2lem4  5343  reusv2  5345  rabxfrd  5359  fimarab  6914  riotaxfrd  7358  tfis  7806  rankr1ai  9722  cfval2  10182  cflim3  10184  cflim2  10185  cfss  10187  cfslb  10188  cofsmo  10191  nnwos  12865  ramval  16979  ramub1lem1  16997  neiptopnei  23097  dissnlocfin  23494  hauseqlcld  23611  imasnopn  23655  imasncld  23656  imasncls  23657  ptcmplem4  24020  blval2  24527  psmetutop  24532  rrxbasefi  25377  mbfinf  25632  itg2monolem1  25717  lhop1  25981  sltsleft  27852  sltsright  27853  ltslpss  27900  cofcutr  27916  cofcutrtime  27919  addsproplem2  27962  rusgrnumwwlkb0  30042  difrab2  32567  aciunf1  32736  fpwrelmap  32806  cntrval2  33232  ply1mulrtss  33642  algextdeglem6  33866  constrfin  33890  locfinreflem  33984  zarcls  34018  ordtconnlem1  34068  fsumcvg4  34094  esumrnmpt2  34212  esumpinfval  34217  hasheuni  34229  measvuni  34358  eulerpartlemn  34525  elorvc  34604  ballotlemimin  34650  ballotlem7  34680  ballotth  34682  reprinrn  34762  reprpmtf1o  34770  reprdifc  34771  bnj1204  35154  bj-rabtrALT  37238  icorempo  37667  isbasisrelowllem1  37671  isbasisrelowllem2  37672  relowlssretop  37679  phpreu  37925  poimirlem26  37967  mbfposadd  37988  cover2  38036  aaitgo  43590  rababg  44001  nznngen  44743  permaxsep  45434  rfcnpre1  45450  rfcnpre2  45462  rabidim2  45532  rabidd  45585  disjf1o  45621  mptssid  45670  infnsuprnmpt  45679  allbutfiinf  45848  supminfxr2  45897  pimxrneun  45916  fsumsupp0  46008  limsupequzmpt2  46146  liminfequzmpt2  46219  cncfshift  46302  cncfperiod  46307  dvcosre  46340  dvnprodlem1  46374  itgsinexplem1  46382  stoweidlem27  46455  stoweidlem31  46459  stoweidlem34  46462  stoweidlem35  46463  stoweidlem59  46487  fourierdlem31  46566  etransclem32  46694  etransclem35  46697  etransclem37  46699  etransclem38  46700  sge0iunmptlemre  46843  meadjiunlem  46893  ovncvrrp  46992  hoidmv1lelem1  47019  hoidmvlelem2  47024  ovnhoilem2  47030  opnvonmbllem2  47061  ovolval4lem1  47077  preimagelt  47127  preimalegt  47128  pimconstlt1  47130  pimltpnff  47131  pimrecltpos  47136  pimgtmnff  47150  pimrecltneg  47152  sssmf  47166  smfaddlem1  47191  smflimlem2  47200  smfmullem4  47222  smflimsuplem4  47251  smflimsuplem7  47254