Theorem rspa 3226

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

Assertion

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

Proof of Theorem rspa

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

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

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 3052

This theorem is referenced by:  r19.21bi  3229  mpteq12f  5170  reusv2lem2  5341  fompt  7070  frrlem12  8247  axdc4lem  10377  fprodle  15961  isucn2  24243  bcthlem5  25295  gausslemma2dlem6  27335  opreu2reuALT  32546  foresf1o  32574  abrexss  32582  iinabrex  32639  reff  33983  locfinreflem  33984  cmpcref  33994  zarclsiin  34015  ldgenpisyslem1  34307  voliune  34373  volfiniune  34374  reprpmtf1o  34770  bnj1366  34971  weiunfrlem  36646  heicant  37976  indexdom  38055  glbconxN  39824  pmapglbx  40215  pmapglb2xN  40218  mzpexpmpt  43177  uzwo4  45484  ralimralim  45512  eliinid  45541  suprnmpt  45604  wessf1ornlem  45615  disjinfi  45622  choicefi  45629  axccdom  45651  axccd  45658  rnmptlb  45672  rnmptbddlem  45673  rnmptbd2lem  45677  upbdrech  45738  ssfiunibd  45742  iuneqfzuzlem  45764  xrralrecnnle  45812  supxrunb3  45828  supxrleubrnmpt  45834  unb2ltle  45843  rexabslelem  45846  suprleubrnmpt  45850  uzublem  45858  infxrgelbrnmpt  45882  cvgcaule  45919  fprodcnlem  46029  limcrecl  46059  islpcn  46067  limsupre  46069  limcleqr  46072  0ellimcdiv  46077  limclner  46079  climinf2lem  46134  climinf3  46144  limsupmnflem  46148  limsupmnfuzlem  46154  limsupre3uzlem  46163  climisp  46174  climrescn  46176  climxrrelem  46177  climxrre  46178  climxlim2lem  46273  cncfshift  46302  cncfperiod  46307  cncfuni  46314  cncfioobd  46325  dvbdfbdioolem1  46356  dvnprodlem2  46375  stoweidlem28  46456  stoweidlem29  46457  stoweidlem31  46459  stoweidlem60  46488  stoweidlem62  46490  fourierdlem39  46574  fourierdlem68  46602  fourierdlem73  46607  fourierdlem77  46611  fourierdlem80  46614  fourierdlem83  46617  fourierdlem87  46621  fourierdlem94  46628  fourierdlem103  46637  fourierdlem104  46638  fourierdlem112  46646  fourierdlem113  46647  qndenserrnbllem  46722  dfsalgen2  46769  subsaliuncl  46786  sge0lefi  46826  sge0isum  46855  sge0reuzb  46876  iundjiun  46888  voliunsge0lem  46900  meaiuninclem  46908  meaiuninc3v  46912  isomenndlem  46958  ovnsubaddlem2  46999  hoidmvlelem3  47025  hoidmvlelem5  47027  hspdifhsp  47044  hoiqssbllem3  47052  hspmbllem2  47055  vonioo  47110  vonicc  47113  pimdecfgtioo  47145  issmflem  47155  issmfle  47173  issmfgt  47184  issmfgelem  47197  smflimlem2  47200  smfinflem  47245  smflimsuplem5  47252  smfliminflem  47258  fsupdm  47270  finfdm  47274  sbgoldbm  48260  sbgoldbo  48263  aacllem  50276