Theorem rabid 3444

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

Syntax hints:   ↔ wb 209   ∧ wa 400   ∈ wcel 2149  {crab 3423

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424

This theorem is referenced by:  rabidim1  3445  reqabi  3446  rabrab  3447  rabss3d  4043  eqrrabd  4048  reusv2lem4  5373  reusv2  5375  rabxfrd  5389  fimarab  6956  riotaxfrd  7402  tfis  7850  rankr1ai  9769  cfval2  10243  cflim3  10245  cflim2  10246  cfss  10248  cfslb  10249  cofsmo  10252  nnwos  12938  ramval  17067  ramub1lem1  17085  neiptopnei  23257  dissnlocfin  23654  hauseqlcld  23771  imasnopn  23815  imasncld  23816  imasncls  23817  ptcmplem4  24180  blval2  24687  psmetutop  24692  rrxbasefi  25537  mbfinf  25792  itg2monolem1  25877  lhop1  26141  sltsleft  28018  sltsright  28019  ltslpss  28066  cofcutr  28082  cofcutrtime  28085  addsproplem2  28128  rusgrnumwwlkb0  30263  difrab2  32784  aciunf1  32948  fpwrelmap  33018  cntrval2  33431  ply1mulrtss  33816  algextdeglem6  34056  constrfin  34080  locfinreflem  34174  zarcls  34208  ordtconnlem1  34258  fsumcvg4  34284  esumrnmpt2  34402  esumpinfval  34407  hasheuni  34419  measvuni  34548  eulerpartlemn  34715  elorvc  34794  ballotlemimin  34840  ballotlem7  34870  ballotth  34872  reprinrn  34949  reprpmtf1o  34957  reprdifc  34958  bnj1204  35344  bj-rabtrALT  37454  icorempo  37884  isbasisrelowllem1  37888  isbasisrelowllem2  37889  relowlssretop  37896  phpreu  38142  poimirlem26  38184  mbfposadd  38205  cover2  38253  aaitgo  43780  rababg  44191  nznngen  44917  permaxsep  45607  rfcnpre1  45630  rfcnpre2  45642  rabidim2  45711  rabidd  45764  disjf1o  45800  mptssid  45847  infnsuprnmpt  45856  allbutfiinf  46025  supminfxr2  46074  pimxrneun  46093  fsumsupp0  46185  limsupequzmpt2  46323  liminfequzmpt2  46396  cncfshift  46479  cncfperiod  46484  dvcosre  46517  dvnprodlem1  46551  itgsinexplem1  46559  stoweidlem27  46632  stoweidlem31  46636  stoweidlem34  46639  stoweidlem35  46640  stoweidlem59  46664  fourierdlem31  46743  etransclem32  46871  etransclem35  46874  etransclem37  46876  etransclem38  46877  sge0iunmptlemre  47020  meadjiunlem  47070  ovncvrrp  47169  hoidmv1lelem1  47196  hoidmvlelem2  47201  ovnhoilem2  47207  opnvonmbllem2  47238  ovolval4lem1  47254  preimagelt  47304  preimalegt  47305  pimconstlt1  47307  pimltpnff  47308  pimrecltpos  47313  pimgtmnff  47327  pimrecltneg  47329  smfaddlem1  47368  smflimlem2  47377  smfmullem4  47399  smflimsuplem4  47428  smflimsuplem7  47431