Theorem rabid 3430

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  {crab 3408

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409

This theorem is referenced by:  rabidim1  3431  reqabi  3432  rabrab  3433  rabss3d  4047  eqrrabd  4052  reusv2lem4  5359  reusv2  5361  rabxfrd  5375  fimarab  6938  riotaxfrd  7381  tfis  7834  rankr1ai  9758  cfval2  10220  cflim3  10222  cflim2  10223  cfss  10225  cfslb  10226  cofsmo  10229  nnwos  12881  ramval  16986  ramub1lem1  17004  neiptopnei  23026  dissnlocfin  23423  hauseqlcld  23540  imasnopn  23584  imasncld  23585  imasncls  23586  ptcmplem4  23949  blval2  24457  psmetutop  24462  rrxbasefi  25317  mbfinf  25573  itg2monolem1  25658  lhop1  25926  ssltleft  27789  ssltright  27790  sltlpss  27826  cofcutr  27839  cofcutrtime  27842  addsproplem2  27884  rusgrnumwwlkb0  29908  difrab2  32434  aciunf1  32594  fpwrelmap  32663  cntrval2  33135  ply1mulrtss  33557  algextdeglem6  33719  constrfin  33743  locfinreflem  33837  zarcls  33871  ordtconnlem1  33921  fsumcvg4  33947  esumrnmpt2  34065  esumpinfval  34070  hasheuni  34082  measvuni  34211  eulerpartlemn  34379  elorvc  34458  ballotlemimin  34504  ballotlem7  34534  ballotth  34536  reprinrn  34616  reprpmtf1o  34624  reprdifc  34625  bnj1204  35009  bj-rabtrALT  36926  icorempo  37346  isbasisrelowllem1  37350  isbasisrelowllem2  37351  relowlssretop  37358  phpreu  37605  poimirlem26  37647  mbfposadd  37668  cover2  37716  aaitgo  43158  rababg  43570  nznngen  44312  permaxsep  45004  rfcnpre1  45020  rfcnpre2  45032  rabidim2  45103  rabidd  45156  disjf1o  45192  mptssid  45242  infnsuprnmpt  45251  allbutfiinf  45423  supminfxr2  45472  pimxrneun  45491  fsumsupp0  45583  limsupequzmpt2  45723  liminfequzmpt2  45796  cncfshift  45879  cncfperiod  45884  dvcosre  45917  dvnprodlem1  45951  itgsinexplem1  45959  stoweidlem27  46032  stoweidlem31  46036  stoweidlem34  46039  stoweidlem35  46040  stoweidlem59  46064  fourierdlem31  46143  etransclem32  46271  etransclem35  46274  etransclem37  46276  etransclem38  46277  sge0iunmptlemre  46420  meadjiunlem  46470  ovncvrrp  46569  hoidmv1lelem1  46596  hoidmvlelem2  46601  ovnhoilem2  46607  opnvonmbllem2  46638  ovolval4lem1  46654  preimagelt  46704  preimalegt  46705  pimconstlt1  46707  pimltpnff  46708  pimrecltpos  46713  pimiooltgt  46715  preimageiingt  46725  preimaleiinlt  46726  pimgtmnff  46727  pimrecltneg  46729  sssmf  46743  smfaddlem1  46768  smflimlem2  46777  smfmullem4  46799  smflimsuplem4  46828  smflimsuplem7  46831