Theorem rabid 3381

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

Syntax hints:   ↔ wb 208   ∧ wa 398   ∈ wcel 2113  {crab 3145

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1539  df-ex 1780  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-rab 3150

This theorem is referenced by:  rabrab  3382  rabidim1  3383  rabeq2i  3490  reusv2lem4  5305  reusv2  5307  rabxfrd  5321  riotaxfrd  7151  tfis  7572  rankr1ai  9230  cfval2  9685  cflim3  9687  cflim2  9688  cfss  9690  cfslb  9691  cofsmo  9694  nnwos  12318  ramval  16347  ramub1lem1  16365  neiptopnei  21743  dissnlocfin  22140  hauseqlcld  22257  imasnopn  22301  imasncld  22302  imasncls  22303  ptcmplem4  22666  blval2  23175  psmetutop  23180  rrxbasefi  24016  mbfinf  24269  itg2monolem1  24354  lhop1  24614  rusgrnumwwlkb0  27753  difrab2  30264  rabss3d  30279  fimarab  30393  aciunf1  30411  fpwrelmap  30472  locfinreflem  31108  ordtconnlem1  31171  fsumcvg4  31197  esumrnmpt2  31331  esumpinfval  31336  hasheuni  31348  measvuni  31477  eulerpartlemn  31643  elorvc  31721  ballotlemimin  31767  ballotlem7  31797  ballotth  31799  reprinrn  31893  reprpmtf1o  31901  reprdifc  31902  bnj1204  32288  bj-rabtrALT  34253  icorempo  34636  isbasisrelowllem1  34640  isbasisrelowllem2  34641  relowlssretop  34648  phpreu  34880  poimirlem26  34922  mbfposadd  34943  cover2  34993  aaitgo  39768  rababg  39939  nznngen  40654  rfcnpre1  41282  rfcnpre2  41294  rabidim2  41374  disjf1o  41458  mptssid  41517  infnsuprnmpt  41528  allbutfiinf  41700  supminfxr2  41751  fsumsupp0  41865  limsupequzmpt2  42005  liminfequzmpt2  42078  cncfshift  42163  cncfperiod  42168  dvcosre  42202  dvnprodlem1  42237  itgsinexplem1  42245  stoweidlem27  42319  stoweidlem31  42323  stoweidlem34  42326  stoweidlem35  42327  stoweidlem59  42351  fourierdlem31  42430  etransclem32  42558  etransclem35  42561  etransclem37  42563  etransclem38  42564  sge0iunmptlemre  42704  meadjiunlem  42754  ovncvrrp  42853  hoidmv1lelem1  42880  hoidmvlelem2  42885  ovnhoilem2  42891  opnvonmbllem2  42922  ovolval4lem1  42938  preimagelt  42987  preimalegt  42988  pimconstlt1  42990  pimltpnf  42991  pimrecltpos  42994  pimiooltgt  42996  preimageiingt  43005  preimaleiinlt  43006  pimrecltneg  43008  sssmf  43022  smfaddlem1  43046  smflimlem2  43055  smfmullem4  43076  smflimsuplem4  43104  smflimsuplem7  43107