Theorem rspa 3227

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

Assertion

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

Proof of Theorem rspa

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3052

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-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-ral 3053

This theorem is referenced by:  r19.21bi  3230  mpteq12f  5185  reusv2lem2  5346  fompt  7072  frrlem12  8249  axdc4lem  10377  fprodle  15931  isucn2  24234  bcthlem5  25296  gausslemma2dlem6  27351  opreu2reuALT  32563  foresf1o  32591  abrexss  32599  iinabrex  32656  reff  34017  locfinreflem  34018  cmpcref  34028  zarclsiin  34049  ldgenpisyslem1  34341  voliune  34407  volfiniune  34408  reprpmtf1o  34804  bnj1366  35005  weiunfrlem  36680  heicant  37906  indexdom  37985  glbconxN  39754  pmapglbx  40145  pmapglb2xN  40148  mzpexpmpt  43102  uzwo4  45413  ralimralim  45441  eliinid  45470  suprnmpt  45533  wessf1ornlem  45544  disjinfi  45551  choicefi  45558  axccdom  45580  axccd  45587  rnmptlb  45601  rnmptbddlem  45602  rnmptbd2lem  45606  upbdrech  45667  ssfiunibd  45671  iuneqfzuzlem  45693  xrralrecnnle  45741  supxrunb3  45757  supxrleubrnmpt  45764  unb2ltle  45773  rexabslelem  45776  suprleubrnmpt  45780  uzublem  45788  infxrgelbrnmpt  45812  cvgcaule  45849  fprodcnlem  45959  limcrecl  45989  islpcn  45997  limsupre  45999  limcleqr  46002  0ellimcdiv  46007  limclner  46009  climinf2lem  46064  climinf3  46074  limsupmnflem  46078  limsupmnfuzlem  46084  limsupre3uzlem  46093  climisp  46104  climrescn  46106  climxrrelem  46107  climxrre  46108  climxlim2lem  46203  cncfshift  46232  cncfperiod  46237  cncfuni  46244  cncfioobd  46255  dvbdfbdioolem1  46286  dvnprodlem2  46305  stoweidlem28  46386  stoweidlem29  46387  stoweidlem31  46389  stoweidlem60  46418  stoweidlem62  46420  fourierdlem39  46504  fourierdlem68  46532  fourierdlem73  46537  fourierdlem77  46541  fourierdlem80  46544  fourierdlem83  46547  fourierdlem87  46551  fourierdlem94  46558  fourierdlem103  46567  fourierdlem104  46568  fourierdlem112  46576  fourierdlem113  46577  qndenserrnbllem  46652  dfsalgen2  46699  subsaliuncl  46716  sge0lefi  46756  sge0isum  46785  sge0reuzb  46806  iundjiun  46818  voliunsge0lem  46830  meaiuninclem  46838  meaiuninc3v  46842  isomenndlem  46888  ovnsubaddlem2  46929  hoidmvlelem3  46955  hoidmvlelem5  46957  hspdifhsp  46974  hoiqssbllem3  46982  hspmbllem2  46985  vonioo  47040  vonicc  47043  pimdecfgtioo  47075  issmflem  47085  issmfle  47103  issmfgt  47114  issmfgelem  47127  smflimlem2  47130  smfinflem  47175  smflimsuplem5  47182  smfliminflem  47188  fsupdm  47200  finfdm  47204  sbgoldbm  48144  sbgoldbo  48147  aacllem  50160