Theorem rabid 3418

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

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

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 2182  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398

This theorem is referenced by:  rabidim1  3419  reqabi  3420  rabrab  3421  rabss3d  4031  eqrrabd  4036  reusv2lem4  5344  reusv2  5346  rabxfrd  5360  fimarab  6906  riotaxfrd  7347  tfis  7795  rankr1ai  9708  cfval2  10168  cflim3  10170  cflim2  10171  cfss  10173  cfslb  10174  cofsmo  10177  nnwos  12826  ramval  16934  ramub1lem1  16952  neiptopnei  23074  dissnlocfin  23471  hauseqlcld  23588  imasnopn  23632  imasncld  23633  imasncls  23634  ptcmplem4  23997  blval2  24504  psmetutop  24509  rrxbasefi  25364  mbfinf  25620  itg2monolem1  25705  lhop1  25973  ssltleft  27842  ssltright  27843  sltlpss  27880  cofcutr  27895  cofcutrtime  27898  addsproplem2  27940  rusgrnumwwlkb0  29996  difrab2  32521  aciunf1  32690  fpwrelmap  32761  cntrval2  33202  ply1mulrtss  33612  algextdeglem6  33828  constrfin  33852  locfinreflem  33946  zarcls  33980  ordtconnlem1  34030  fsumcvg4  34056  esumrnmpt2  34174  esumpinfval  34179  hasheuni  34191  measvuni  34320  eulerpartlemn  34487  elorvc  34566  ballotlemimin  34612  ballotlem7  34642  ballotth  34644  reprinrn  34724  reprpmtf1o  34732  reprdifc  34733  bnj1204  35117  bj-rabtrALT  37075  icorempo  37495  isbasisrelowllem1  37499  isbasisrelowllem2  37500  relowlssretop  37507  phpreu  37744  poimirlem26  37786  mbfposadd  37807  cover2  37855  aaitgo  43346  rababg  43757  nznngen  44499  permaxsep  45190  rfcnpre1  45206  rfcnpre2  45218  rabidim2  45288  rabidd  45341  disjf1o  45377  mptssid  45427  infnsuprnmpt  45436  allbutfiinf  45606  supminfxr2  45655  pimxrneun  45674  fsumsupp0  45766  limsupequzmpt2  45904  liminfequzmpt2  45977  cncfshift  46060  cncfperiod  46065  dvcosre  46098  dvnprodlem1  46132  itgsinexplem1  46140  stoweidlem27  46213  stoweidlem31  46217  stoweidlem34  46220  stoweidlem35  46221  stoweidlem59  46245  fourierdlem31  46324  etransclem32  46452  etransclem35  46455  etransclem37  46457  etransclem38  46458  sge0iunmptlemre  46601  meadjiunlem  46651  ovncvrrp  46750  hoidmv1lelem1  46777  hoidmvlelem2  46782  ovnhoilem2  46788  opnvonmbllem2  46819  ovolval4lem1  46835  preimagelt  46885  preimalegt  46886  pimconstlt1  46888  pimltpnff  46889  pimrecltpos  46894  pimgtmnff  46908  pimrecltneg  46910  sssmf  46924  smfaddlem1  46949  smflimlem2  46958  smfmullem4  46980  smflimsuplem4  47009  smflimsuplem7  47012