Theorem rabid 3378

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

Syntax hints:   ↔ wb 208   ∧ wa 398   ∈ wcel 2110  {crab 3142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1536  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147

This theorem is referenced by:  rabrab  3379  rabidim1  3380  rabeq2i  3487  reusv2lem4  5301  reusv2  5303  rabxfrd  5317  riotaxfrd  7147  tfis  7568  rankr1ai  9226  cfval2  9681  cflim3  9683  cflim2  9684  cfss  9686  cfslb  9687  cofsmo  9690  nnwos  12314  ramval  16343  ramub1lem1  16361  neiptopnei  21739  dissnlocfin  22136  hauseqlcld  22253  imasnopn  22297  imasncld  22298  imasncls  22299  ptcmplem4  22662  blval2  23171  psmetutop  23176  rrxbasefi  24012  mbfinf  24265  itg2monolem1  24350  lhop1  24610  rusgrnumwwlkb0  27749  difrab2  30260  rabss3d  30275  fimarab  30389  aciunf1  30407  fpwrelmap  30468  locfinreflem  31104  ordtconnlem1  31167  fsumcvg4  31193  esumrnmpt2  31327  esumpinfval  31332  hasheuni  31344  measvuni  31473  eulerpartlemn  31639  elorvc  31717  ballotlemimin  31763  ballotlem7  31793  ballotth  31795  reprinrn  31889  reprpmtf1o  31897  reprdifc  31898  bnj1204  32284  bj-rabtrALT  34249  icorempo  34631  isbasisrelowllem1  34635  isbasisrelowllem2  34636  relowlssretop  34643  phpreu  34875  poimirlem26  34917  mbfposadd  34938  cover2  34988  aaitgo  39760  rababg  39931  nznngen  40646  rfcnpre1  41274  rfcnpre2  41286  rabidim2  41366  disjf1o  41450  mptssid  41509  infnsuprnmpt  41520  allbutfiinf  41692  supminfxr2  41743  fsumsupp0  41857  limsupequzmpt2  41997  liminfequzmpt2  42070  cncfshift  42155  cncfperiod  42160  dvcosre  42194  dvnprodlem1  42229  itgsinexplem1  42237  stoweidlem27  42311  stoweidlem31  42315  stoweidlem34  42318  stoweidlem35  42319  stoweidlem59  42343  fourierdlem31  42422  etransclem32  42550  etransclem35  42553  etransclem37  42555  etransclem38  42556  sge0iunmptlemre  42696  meadjiunlem  42746  ovncvrrp  42845  hoidmv1lelem1  42872  hoidmvlelem2  42877  ovnhoilem2  42883  opnvonmbllem2  42914  ovolval4lem1  42930  preimagelt  42979  preimalegt  42980  pimconstlt1  42982  pimltpnf  42983  pimrecltpos  42986  pimiooltgt  42988  preimageiingt  42997  preimaleiinlt  42998  pimrecltneg  43000  sssmf  43014  smfaddlem1  43038  smflimlem2  43047  smfmullem4  43068  smflimsuplem4  43096  smflimsuplem7  43099