Theorem rabid 3432

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  {crab 3412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413

This theorem is used by:  rabidim1  3433  reqabi  3434  rabrab  3435  rabss3d  4029  eqrrabd  4034  reusv2lem4  5366  reusv2  5368  rabxfrd  5382  fimarab  6953  riotaxfrd  7405  tfis  7852  rankr1ai  9781  cfval2  10263  cflim3  10265  cflim2  10266  cfss  10268  cfslb  10269  cofsmo  10272  nnwos  12965  ramval  17101  ramub1lem1  17119  rspsn0  21436  neiptopnei  23358  dissnlocfin  23756  hauseqlcld  23873  imasnopn  23917  imasncld  23918  imasncls  23919  ptcmplem4  24282  blval2  24789  psmetutop  24794  rrxbasefi  25639  mbfinf  25894  itg2monolem1  25979  lhop1  26242  sltsleft  28126  sltsright  28127  ltslpss  28174  cofcutr  28190  cofcutrtime  28193  addsproplem2  28236  rusgrnumwwlkb0  30443  difrab2  32974  aciunf1  33137  fpwrelmap  33205  cntrval2  33612  ply1mulrtss  33993  algextdeglem6  34233  constrfin  34257  locfinreflem  34351  zarcls  34385  ordtconnlem1  34435  fsumcvg4  34461  esumrnmpt2  34579  esumpinfval  34584  hasheuni  34596  measvuni  34726  eulerpartlemn  34893  elorvc  34972  ballotlemimin  35018  ballotlem7  35048  ballotth  35050  reprinrn  35127  reprpmtf1o  35135  reprdifc  35136  bnj1204  35522  bj-rabtrALT  37676  icorempo  38106  isbasisrelowllem1  38110  isbasisrelowllem2  38111  relowlssretop  38118  phpreu  38359  poimirlem26  38396  mbfposadd  38417  cover2  38466  aaitgo  44004  rababg  44415  nznngen  45141  permaxsep  45831  rfcnpre1  45854  rfcnpre2  45866  rabidim2  45935  rabidd  45988  disjf1o  46024  mptssid  46071  infnsuprnmpt  46080  allbutfiinf  46249  supminfxr2  46298  pimxrneun  46317  fsumsupp0  46409  limsupequzmpt2  46547  liminfequzmpt2  46620  cncfshift  46703  cncfperiod  46708  dvcosre  46741  dvnprodlem1  46775  itgsinexplem1  46783  stoweidlem27  46856  stoweidlem31  46860  stoweidlem34  46863  stoweidlem35  46864  stoweidlem59  46888  fourierdlem31  46967  etransclem32  47095  etransclem35  47098  etransclem37  47100  etransclem38  47101  sge0iunmptlemre  47244  meadjiunlem  47294  ovncvrrp  47393  hoidmv1lelem1  47420  hoidmvlelem2  47425  ovnhoilem2  47431  opnvonmbllem2  47462  ovolval4lem1  47478  preimagelt  47528  preimalegt  47529  pimconstlt1  47531  pimltpnff  47532  pimrecltpos  47537  pimgtmnff  47551  pimrecltneg  47553  smfaddlem1  47592  smflimlem2  47601  smfmullem4  47623  smflimsuplem4  47652  smflimsuplem7  47655