Theorem rabid 3408

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  {crab 3387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2184  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3388

This theorem is referenced by:  rabidim1  3409  reqabi  3410  rabrab  3411  rabss3d  4014  eqrrabd  4019  reusv2lem4  5332  reusv2  5334  rabxfrd  5348  fimarab  6903  riotaxfrd  7347  tfis  7795  rankr1ai  9711  cfval2  10171  cflim3  10173  cflim2  10174  cfss  10176  cfslb  10177  cofsmo  10180  nnwos  12854  ramval  16968  ramub1lem1  16986  neiptopnei  23085  dissnlocfin  23482  hauseqlcld  23599  imasnopn  23643  imasncld  23644  imasncls  23645  ptcmplem4  24008  blval2  24515  psmetutop  24520  rrxbasefi  25365  mbfinf  25620  itg2monolem1  25705  lhop1  25969  sltsleft  27840  sltsright  27841  ltslpss  27888  cofcutr  27904  cofcutrtime  27907  addsproplem2  27950  rusgrnumwwlkb0  30030  difrab2  32555  aciunf1  32724  fpwrelmap  32794  cntrval2  33220  ply1mulrtss  33630  algextdeglem6  33854  constrfin  33878  locfinreflem  33972  zarcls  34006  ordtconnlem1  34056  fsumcvg4  34082  esumrnmpt2  34200  esumpinfval  34205  hasheuni  34217  measvuni  34346  eulerpartlemn  34513  elorvc  34592  ballotlemimin  34638  ballotlem7  34668  ballotth  34670  reprinrn  34750  reprpmtf1o  34758  reprdifc  34759  bnj1204  35142  bj-rabtrALT  37226  icorempo  37655  isbasisrelowllem1  37659  isbasisrelowllem2  37660  relowlssretop  37667  phpreu  37913  poimirlem26  37955  mbfposadd  37976  cover2  38024  aaitgo  43578  rababg  43989  nznngen  44731  permaxsep  45422  rfcnpre1  45438  rfcnpre2  45450  rabidim2  45520  rabidd  45573  disjf1o  45609  mptssid  45658  infnsuprnmpt  45667  allbutfiinf  45836  supminfxr2  45885  pimxrneun  45904  fsumsupp0  45996  limsupequzmpt2  46134  liminfequzmpt2  46207  cncfshift  46290  cncfperiod  46295  dvcosre  46328  dvnprodlem1  46362  itgsinexplem1  46370  stoweidlem27  46443  stoweidlem31  46447  stoweidlem34  46450  stoweidlem35  46451  stoweidlem59  46475  fourierdlem31  46554  etransclem32  46682  etransclem35  46685  etransclem37  46687  etransclem38  46688  sge0iunmptlemre  46831  meadjiunlem  46881  ovncvrrp  46980  hoidmv1lelem1  47007  hoidmvlelem2  47012  ovnhoilem2  47018  opnvonmbllem2  47049  ovolval4lem1  47065  preimagelt  47115  preimalegt  47116  pimconstlt1  47118  pimltpnff  47119  pimrecltpos  47124  pimgtmnff  47138  pimrecltneg  47140  sssmf  47154  smfaddlem1  47179  smflimlem2  47188  smfmullem4  47210  smflimsuplem4  47239  smflimsuplem7  47242