Theorem rabid 3420

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2113  {crab 3399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400

This theorem is referenced by:  rabidim1  3421  reqabi  3422  rabrab  3423  rabss3d  4033  eqrrabd  4038  reusv2lem4  5346  reusv2  5348  rabxfrd  5362  fimarab  6908  riotaxfrd  7349  tfis  7797  rankr1ai  9710  cfval2  10170  cflim3  10172  cflim2  10173  cfss  10175  cfslb  10176  cofsmo  10179  nnwos  12828  ramval  16936  ramub1lem1  16954  neiptopnei  23076  dissnlocfin  23473  hauseqlcld  23590  imasnopn  23634  imasncld  23635  imasncls  23636  ptcmplem4  23999  blval2  24506  psmetutop  24511  rrxbasefi  25366  mbfinf  25622  itg2monolem1  25707  lhop1  25975  sltsleft  27856  sltsright  27857  ltslpss  27904  cofcutr  27920  cofcutrtime  27923  addsproplem2  27966  rusgrnumwwlkb0  30047  difrab2  32572  aciunf1  32741  fpwrelmap  32812  cntrval2  33253  ply1mulrtss  33663  algextdeglem6  33879  constrfin  33903  locfinreflem  33997  zarcls  34031  ordtconnlem1  34081  fsumcvg4  34107  esumrnmpt2  34225  esumpinfval  34230  hasheuni  34242  measvuni  34371  eulerpartlemn  34538  elorvc  34617  ballotlemimin  34663  ballotlem7  34693  ballotth  34695  reprinrn  34775  reprpmtf1o  34783  reprdifc  34784  bnj1204  35168  bj-rabtrALT  37132  icorempo  37556  isbasisrelowllem1  37560  isbasisrelowllem2  37561  relowlssretop  37568  phpreu  37805  poimirlem26  37847  mbfposadd  37868  cover2  37916  aaitgo  43404  rababg  43815  nznngen  44557  permaxsep  45248  rfcnpre1  45264  rfcnpre2  45276  rabidim2  45346  rabidd  45399  disjf1o  45435  mptssid  45485  infnsuprnmpt  45494  allbutfiinf  45664  supminfxr2  45713  pimxrneun  45732  fsumsupp0  45824  limsupequzmpt2  45962  liminfequzmpt2  46035  cncfshift  46118  cncfperiod  46123  dvcosre  46156  dvnprodlem1  46190  itgsinexplem1  46198  stoweidlem27  46271  stoweidlem31  46275  stoweidlem34  46278  stoweidlem35  46279  stoweidlem59  46303  fourierdlem31  46382  etransclem32  46510  etransclem35  46513  etransclem37  46515  etransclem38  46516  sge0iunmptlemre  46659  meadjiunlem  46709  ovncvrrp  46808  hoidmv1lelem1  46835  hoidmvlelem2  46840  ovnhoilem2  46846  opnvonmbllem2  46877  ovolval4lem1  46893  preimagelt  46943  preimalegt  46944  pimconstlt1  46946  pimltpnff  46947  pimrecltpos  46952  pimgtmnff  46966  pimrecltneg  46968  sssmf  46982  smfaddlem1  47007  smflimlem2  47016  smfmullem4  47038  smflimsuplem4  47067  smflimsuplem7  47070