Theorem rabid 3435

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

Syntax hints:   ↔ wb 208   ∧ wa 399   ∈ wcel 2142  {crab 3414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-12 2212  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415

This theorem is referenced by:  rabidim1  3436  reqabi  3437  rabrab  3438  rabss3d  4034  eqrrabd  4039  reusv2lem4  5358  reusv2  5360  rabxfrd  5374  fimarab  6941  riotaxfrd  7387  tfis  7835  rankr1ai  9756  cfval2  10217  cflim3  10219  cflim2  10220  cfss  10222  cfslb  10223  cofsmo  10226  nnwos  12916  ramval  17044  ramub1lem1  17062  neiptopnei  23192  dissnlocfin  23589  hauseqlcld  23706  imasnopn  23750  imasncld  23751  imasncls  23752  ptcmplem4  24115  blval2  24622  psmetutop  24627  rrxbasefi  25472  mbfinf  25727  itg2monolem1  25812  lhop1  26076  sltsleft  27953  sltsright  27954  ltslpss  28001  cofcutr  28017  cofcutrtime  28020  addsproplem2  28063  rusgrnumwwlkb0  30174  difrab2  32697  aciunf1  32865  fpwrelmap  32935  cntrval2  33351  ply1mulrtss  33778  algextdeglem6  34019  constrfin  34043  locfinreflem  34137  zarcls  34171  ordtconnlem1  34221  fsumcvg4  34247  esumrnmpt2  34365  esumpinfval  34370  hasheuni  34382  measvuni  34511  eulerpartlemn  34678  elorvc  34757  ballotlemimin  34803  ballotlem7  34833  ballotth  34835  reprinrn  34912  reprpmtf1o  34920  reprdifc  34921  bnj1204  35307  bj-rabtrALT  37416  icorempo  37845  isbasisrelowllem1  37849  isbasisrelowllem2  37850  relowlssretop  37857  phpreu  38103  poimirlem26  38145  mbfposadd  38166  cover2  38214  aaitgo  43739  rababg  44150  nznngen  44892  permaxsep  45583  rfcnpre1  45599  rfcnpre2  45611  rabidim2  45680  rabidd  45733  disjf1o  45769  mptssid  45816  infnsuprnmpt  45825  allbutfiinf  45994  supminfxr2  46043  pimxrneun  46062  fsumsupp0  46154  limsupequzmpt2  46292  liminfequzmpt2  46365  cncfshift  46448  cncfperiod  46453  dvcosre  46486  dvnprodlem1  46520  itgsinexplem1  46528  stoweidlem27  46601  stoweidlem31  46605  stoweidlem34  46608  stoweidlem35  46609  stoweidlem59  46633  fourierdlem31  46712  etransclem32  46840  etransclem35  46843  etransclem37  46845  etransclem38  46846  sge0iunmptlemre  46989  meadjiunlem  47039  ovncvrrp  47138  hoidmv1lelem1  47165  hoidmvlelem2  47170  ovnhoilem2  47176  opnvonmbllem2  47207  ovolval4lem1  47223  preimagelt  47273  preimalegt  47274  pimconstlt1  47276  pimltpnff  47277  pimrecltpos  47282  pimgtmnff  47296  pimrecltneg  47298  smfaddlem1  47337  smflimlem2  47346  smfmullem4  47368  smflimsuplem4  47397  smflimsuplem7  47400