Theorem rabid 3422

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

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

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 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402

This theorem is referenced by:  rabidim1  3423  reqabi  3424  rabrab  3425  rabss3d  4035  eqrrabd  4040  reusv2lem4  5348  reusv2  5350  rabxfrd  5364  fimarab  6916  riotaxfrd  7359  tfis  7807  rankr1ai  9722  cfval2  10182  cflim3  10184  cflim2  10185  cfss  10187  cfslb  10188  cofsmo  10191  nnwos  12840  ramval  16948  ramub1lem1  16966  neiptopnei  23088  dissnlocfin  23485  hauseqlcld  23602  imasnopn  23646  imasncld  23647  imasncls  23648  ptcmplem4  24011  blval2  24518  psmetutop  24523  rrxbasefi  25378  mbfinf  25634  itg2monolem1  25719  lhop1  25987  sltsleft  27868  sltsright  27869  ltslpss  27916  cofcutr  27932  cofcutrtime  27935  addsproplem2  27978  rusgrnumwwlkb0  30059  difrab2  32584  aciunf1  32753  fpwrelmap  32823  cntrval2  33265  ply1mulrtss  33675  algextdeglem6  33900  constrfin  33924  locfinreflem  34018  zarcls  34052  ordtconnlem1  34102  fsumcvg4  34128  esumrnmpt2  34246  esumpinfval  34251  hasheuni  34263  measvuni  34392  eulerpartlemn  34559  elorvc  34638  ballotlemimin  34684  ballotlem7  34714  ballotth  34716  reprinrn  34796  reprpmtf1o  34804  reprdifc  34805  bnj1204  35188  bj-rabtrALT  37179  icorempo  37606  isbasisrelowllem1  37610  isbasisrelowllem2  37611  relowlssretop  37618  phpreu  37855  poimirlem26  37897  mbfposadd  37918  cover2  37966  aaitgo  43519  rababg  43930  nznngen  44672  permaxsep  45363  rfcnpre1  45379  rfcnpre2  45391  rabidim2  45461  rabidd  45514  disjf1o  45550  mptssid  45599  infnsuprnmpt  45608  allbutfiinf  45778  supminfxr2  45827  pimxrneun  45846  fsumsupp0  45938  limsupequzmpt2  46076  liminfequzmpt2  46149  cncfshift  46232  cncfperiod  46237  dvcosre  46270  dvnprodlem1  46304  itgsinexplem1  46312  stoweidlem27  46385  stoweidlem31  46389  stoweidlem34  46392  stoweidlem35  46393  stoweidlem59  46417  fourierdlem31  46496  etransclem32  46624  etransclem35  46627  etransclem37  46629  etransclem38  46630  sge0iunmptlemre  46773  meadjiunlem  46823  ovncvrrp  46922  hoidmv1lelem1  46949  hoidmvlelem2  46954  ovnhoilem2  46960  opnvonmbllem2  46991  ovolval4lem1  47007  preimagelt  47057  preimalegt  47058  pimconstlt1  47060  pimltpnff  47061  pimrecltpos  47066  pimgtmnff  47080  pimrecltneg  47082  sssmf  47096  smfaddlem1  47121  smflimlem2  47130  smfmullem4  47152  smflimsuplem4  47181  smflimsuplem7  47184