Theorem rspa 3228

Description: Restricted specialization. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Assertion

Ref	Expression
rspa	⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜑)

Proof of Theorem rspa

Step	Hyp	Ref	Expression
1		rsp 3227	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑))
2	1	imp 407	1 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-ral 3054

This theorem is referenced by:  r19.21bi  3231  mpteq12f  5157  reusv2lem2  5328  fompt  7059  frrlem12  8237  axdc4lem  10368  fprodle  15952  isucn2  24261  bcthlem5  25313  gausslemma2dlem6  27353  opreu2reuALT  32564  foresf1o  32592  abrexss  32600  iinabrex  32658  reff  34023  locfinreflem  34024  cmpcref  34034  zarclsiin  34055  ldgenpisyslem1  34347  voliune  34413  volfiniune  34414  reprpmtf1o  34810  bnj1366  35011  weiunfrlem  36692  heicant  38022  indexdom  38101  glbconxN  39870  pmapglbx  40261  pmapglb2xN  40264  mzpexpmpt  43194  uzwo4  45501  ralimralim  45529  eliinid  45558  suprnmpt  45621  wessf1ornlem  45632  disjinfi  45639  choicefi  45646  axccdom  45667  axccd  45673  rnmptlb  45687  rnmptbddlem  45688  rnmptbd2lem  45692  upbdrech  45753  ssfiunibd  45757  iuneqfzuzlem  45779  xrralrecnnle  45827  supxrunb3  45843  supxrleubrnmpt  45849  unb2ltle  45858  rexabslelem  45861  suprleubrnmpt  45865  uzublem  45873  infxrgelbrnmpt  45897  cvgcaule  45934  fprodcnlem  46044  limcrecl  46074  islpcn  46082  limsupre  46084  limcleqr  46087  0ellimcdiv  46092  limclner  46094  climinf2lem  46149  climinf3  46159  limsupmnflem  46163  limsupmnfuzlem  46169  limsupre3uzlem  46178  climisp  46189  climrescn  46191  climxrrelem  46192  climxrre  46193  climxlim2lem  46288  cncfshift  46317  cncfperiod  46322  cncfuni  46329  cncfioobd  46340  dvbdfbdioolem1  46371  dvnprodlem2  46390  stoweidlem28  46471  stoweidlem29  46472  stoweidlem31  46474  stoweidlem60  46503  stoweidlem62  46505  fourierdlem39  46589  fourierdlem68  46617  fourierdlem73  46622  fourierdlem77  46626  fourierdlem80  46629  fourierdlem83  46632  fourierdlem87  46636  fourierdlem94  46643  fourierdlem103  46652  fourierdlem104  46653  fourierdlem112  46661  fourierdlem113  46662  qndenserrnbllem  46737  dfsalgen2  46784  subsaliuncl  46801  sge0lefi  46841  sge0isum  46870  sge0reuzb  46891  iundjiun  46903  voliunsge0lem  46915  meaiuninclem  46923  meaiuninc3v  46927  isomenndlem  46973  ovnsubaddlem2  47014  hoidmvlelem3  47040  hoidmvlelem5  47042  hspdifhsp  47059  hoiqssbllem3  47067  hspmbllem2  47070  vonioo  47125  vonicc  47128  pimdecfgtioo  47160  issmflem  47170  issmfle  47188  issmfgt  47199  issmfgelem  47212  smflimlem2  47215  smfinflem  47260  smflimsuplem5  47267  smfliminflem  47273  fsupdm  47285  finfdm  47289  sbgoldbm  48275  sbgoldbo  48278  aacllem  50291