Theorem rabid 3424

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  {crab 3402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403

This theorem is referenced by:  rabidim1  3425  reqabi  3426  rabrab  3427  rabss3d  4040  eqrrabd  4045  reusv2lem4  5351  reusv2  5353  rabxfrd  5367  fimarab  6917  riotaxfrd  7360  tfis  7811  rankr1ai  9727  cfval2  10189  cflim3  10191  cflim2  10192  cfss  10194  cfslb  10195  cofsmo  10198  nnwos  12850  ramval  16955  ramub1lem1  16973  neiptopnei  22995  dissnlocfin  23392  hauseqlcld  23509  imasnopn  23553  imasncld  23554  imasncls  23555  ptcmplem4  23918  blval2  24426  psmetutop  24431  rrxbasefi  25286  mbfinf  25542  itg2monolem1  25627  lhop1  25895  ssltleft  27758  ssltright  27759  sltlpss  27795  cofcutr  27808  cofcutrtime  27811  addsproplem2  27853  rusgrnumwwlkb0  29874  difrab2  32400  aciunf1  32560  fpwrelmap  32629  cntrval2  33101  ply1mulrtss  33523  algextdeglem6  33685  constrfin  33709  locfinreflem  33803  zarcls  33837  ordtconnlem1  33887  fsumcvg4  33913  esumrnmpt2  34031  esumpinfval  34036  hasheuni  34048  measvuni  34177  eulerpartlemn  34345  elorvc  34424  ballotlemimin  34470  ballotlem7  34500  ballotth  34502  reprinrn  34582  reprpmtf1o  34590  reprdifc  34591  bnj1204  34975  bj-rabtrALT  36892  icorempo  37312  isbasisrelowllem1  37316  isbasisrelowllem2  37317  relowlssretop  37324  phpreu  37571  poimirlem26  37613  mbfposadd  37634  cover2  37682  aaitgo  43124  rababg  43536  nznngen  44278  permaxsep  44970  rfcnpre1  44986  rfcnpre2  44998  rabidim2  45069  rabidd  45122  disjf1o  45158  mptssid  45208  infnsuprnmpt  45217  allbutfiinf  45389  supminfxr2  45438  pimxrneun  45457  fsumsupp0  45549  limsupequzmpt2  45689  liminfequzmpt2  45762  cncfshift  45845  cncfperiod  45850  dvcosre  45883  dvnprodlem1  45917  itgsinexplem1  45925  stoweidlem27  45998  stoweidlem31  46002  stoweidlem34  46005  stoweidlem35  46006  stoweidlem59  46030  fourierdlem31  46109  etransclem32  46237  etransclem35  46240  etransclem37  46242  etransclem38  46243  sge0iunmptlemre  46386  meadjiunlem  46436  ovncvrrp  46535  hoidmv1lelem1  46562  hoidmvlelem2  46567  ovnhoilem2  46573  opnvonmbllem2  46604  ovolval4lem1  46620  preimagelt  46670  preimalegt  46671  pimconstlt1  46673  pimltpnff  46674  pimrecltpos  46679  pimiooltgt  46681  preimageiingt  46691  preimaleiinlt  46692  pimgtmnff  46693  pimrecltneg  46695  sssmf  46709  smfaddlem1  46734  smflimlem2  46743  smfmullem4  46765  smflimsuplem4  46794  smflimsuplem7  46797