Theorem rspa 3130

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

Assertion

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

Proof of Theorem rspa

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-ral 3068

This theorem is referenced by:  r19.21bi  3132  ralimda  3421  dfiun2g  4957  mpteq12f  5158  reusv2lem2  5317  frrlem12  8084  axdc4lem  10142  fprodle  15634  isucn2  23339  bcthlem5  24397  gausslemma2dlem6  26425  opreu2reuALT  30726  foresf1o  30751  abrexss  30758  iinabrex  30809  reff  31691  locfinreflem  31692  cmpcref  31702  zarclsiin  31723  ldgenpisyslem1  32031  voliune  32097  volfiniune  32098  reprpmtf1o  32506  bnj1366  32709  heicant  35739  indexdom  35819  glbconxN  37319  pmapglbx  37710  pmapglb2xN  37713  mzpexpmpt  40483  uzwo4  42490  ralimralim  42520  eliinid  42550  suprnmpt  42599  wessf1ornlem  42611  fompt  42619  disjinfi  42620  choicefi  42629  axccdom  42651  axccd  42657  rnmptlb  42677  rnmptbddlem  42678  rnmptbd2lem  42683  upbdrech  42734  ssfiunibd  42738  iuneqfzuzlem  42763  xrralrecnnle  42812  supxrunb3  42829  supxrleubrnmpt  42836  unb2ltle  42845  rexabslelem  42848  suprleubrnmpt  42852  uzublem  42860  infxrgelbrnmpt  42884  fprodcnlem  43030  limcrecl  43060  islpcn  43070  limsupre  43072  limcleqr  43075  0ellimcdiv  43080  limclner  43082  climinf2lem  43137  climinf3  43147  limsupmnflem  43151  limsupmnfuzlem  43157  limsupre3uzlem  43166  climisp  43177  climrescn  43179  climxrrelem  43180  climxrre  43181  climxlim2lem  43276  cncfshift  43305  cncfperiod  43310  cncfuni  43317  cncfioobd  43328  dvbdfbdioolem1  43359  dvnprodlem2  43378  stoweidlem28  43459  stoweidlem29  43460  stoweidlem31  43462  stoweidlem60  43491  stoweidlem62  43493  fourierdlem39  43577  fourierdlem68  43605  fourierdlem73  43610  fourierdlem77  43614  fourierdlem80  43617  fourierdlem83  43620  fourierdlem87  43624  fourierdlem94  43631  fourierdlem103  43640  fourierdlem104  43641  fourierdlem112  43649  fourierdlem113  43650  qndenserrnbllem  43725  dfsalgen2  43770  subsaliuncl  43787  sge0lefi  43826  sge0isum  43855  sge0reuzb  43876  iundjiun  43888  voliunsge0lem  43900  meaiuninclem  43908  meaiuninc3v  43912  isomenndlem  43958  ovnsubaddlem2  43999  hoidmvlelem3  44025  hoidmvlelem5  44027  hspdifhsp  44044  hoiqssbllem3  44052  hspmbllem2  44055  vonioo  44110  vonicc  44113  pimdecfgtioo  44141  issmflem  44150  issmfle  44168  issmfgt  44179  issmfgelem  44191  smflimlem2  44194  smfinflem  44237  smflimsuplem5  44244  smfliminflem  44250  sbgoldbm  45124  sbgoldbo  45127  aacllem  46391