Theorem rabid 3331

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

Syntax hints:   ↔ wb 209   ∧ wa 399   ∈ wcel 2111  {crab 3110

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115

This theorem is referenced by:  rabrab  3332  rabidim1  3333  rabeq2i  3435  reusv2lem4  5267  reusv2  5269  rabxfrd  5283  riotaxfrd  7127  tfis  7549  rankr1ai  9211  cfval2  9671  cflim3  9673  cflim2  9674  cfss  9676  cfslb  9677  cofsmo  9680  nnwos  12303  ramval  16334  ramub1lem1  16352  neiptopnei  21737  dissnlocfin  22134  hauseqlcld  22251  imasnopn  22295  imasncld  22296  imasncls  22297  ptcmplem4  22660  blval2  23169  psmetutop  23174  rrxbasefi  24014  mbfinf  24269  itg2monolem1  24354  lhop1  24617  rusgrnumwwlkb0  27757  difrab2  30268  eqrrabd  30272  rabss3d  30285  fimarab  30404  aciunf1  30426  fpwrelmap  30495  locfinreflem  31193  zarcls  31227  ordtconnlem1  31277  fsumcvg4  31303  esumrnmpt2  31437  esumpinfval  31442  hasheuni  31454  measvuni  31583  eulerpartlemn  31749  elorvc  31827  ballotlemimin  31873  ballotlem7  31903  ballotth  31905  reprinrn  31999  reprpmtf1o  32007  reprdifc  32008  bnj1204  32394  bj-rabtrALT  34373  icorempo  34768  isbasisrelowllem1  34772  isbasisrelowllem2  34773  relowlssretop  34780  phpreu  35041  poimirlem26  35083  mbfposadd  35104  cover2  35152  aaitgo  40106  rababg  40273  nznngen  41020  rfcnpre1  41648  rfcnpre2  41660  rabidim2  41738  disjf1o  41818  mptssid  41877  infnsuprnmpt  41888  allbutfiinf  42057  supminfxr2  42108  fsumsupp0  42220  limsupequzmpt2  42360  liminfequzmpt2  42433  cncfshift  42516  cncfperiod  42521  dvcosre  42554  dvnprodlem1  42588  itgsinexplem1  42596  stoweidlem27  42669  stoweidlem31  42673  stoweidlem34  42676  stoweidlem35  42677  stoweidlem59  42701  fourierdlem31  42780  etransclem32  42908  etransclem35  42911  etransclem37  42913  etransclem38  42914  sge0iunmptlemre  43054  meadjiunlem  43104  ovncvrrp  43203  hoidmv1lelem1  43230  hoidmvlelem2  43235  ovnhoilem2  43241  opnvonmbllem2  43272  ovolval4lem1  43288  preimagelt  43337  preimalegt  43338  pimconstlt1  43340  pimltpnf  43341  pimrecltpos  43344  pimiooltgt  43346  preimageiingt  43355  preimaleiinlt  43356  pimrecltneg  43358  sssmf  43372  smfaddlem1  43396  smflimlem2  43405  smfmullem4  43426  smflimsuplem4  43454  smflimsuplem7  43457