Theorem rspa 3173

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

Assertion

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

Proof of Theorem rspa

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2081  ∀wral 3105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-12 2141

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-ral 3110

This theorem is referenced by:  r19.21bi  3175  ralbiOLD  3197  ralrexbidOLD  3284  dfiun2g  4858  mpteq12f  5043  reusv2lem2  5191  axdc4lem  9723  fprodle  15183  isucn2  22571  bcthlem5  23614  gausslemma2dlem6  25630  opreu2reuALT  29932  foresf1o  29957  abrexss  29964  reff  30720  locfinreflem  30721  cmpcref  30731  ldgenpisyslem1  31039  voliune  31105  volfiniune  31106  reprpmtf1o  31514  bnj1366  31718  frrlem12  32743  heicant  34458  indexdom  34541  glbconxN  36045  pmapglbx  36436  pmapglb2xN  36439  mzpexpmpt  38827  uzwo4  40854  ralimralim  40884  eliinid  40917  ralimda  40945  suprnmpt  40970  wessf1ornlem  40985  fompt  40993  disjinfi  40994  choicefi  41003  axccdom  41027  axccd  41035  rnmptlb  41055  rnmptbddlem  41056  rnmptbd2lem  41061  upbdrech  41113  ssfiunibd  41117  iuneqfzuzlem  41143  xrralrecnnle  41194  supxrunb3  41213  supxrleubrnmpt  41221  unb2ltle  41231  rexabslelem  41234  suprleubrnmpt  41238  uzublem  41246  infxrgelbrnmpt  41272  fprodcnlem  41422  limcrecl  41452  islpcn  41462  limsupre  41464  limcleqr  41467  0ellimcdiv  41472  limclner  41474  climinf2lem  41529  climinf3  41539  limsupmnflem  41543  limsupmnfuzlem  41549  limsupre3uzlem  41558  climisp  41569  climrescn  41571  climxrrelem  41572  climxrre  41573  climxlim2lem  41668  cncfshift  41698  cncfperiod  41703  cncfuni  41710  cncfioobd  41721  dvbdfbdioolem1  41754  dvnprodlem2  41773  stoweidlem28  41855  stoweidlem29  41856  stoweidlem31  41858  stoweidlem60  41887  stoweidlem62  41889  fourierdlem39  41973  fourierdlem68  42001  fourierdlem73  42006  fourierdlem77  42010  fourierdlem80  42013  fourierdlem83  42016  fourierdlem87  42020  fourierdlem94  42027  fourierdlem103  42036  fourierdlem104  42037  fourierdlem112  42045  fourierdlem113  42046  qndenserrnbllem  42121  dfsalgen2  42166  subsaliuncl  42183  sge0lefi  42222  sge0isum  42251  sge0reuzb  42272  iundjiun  42284  voliunsge0lem  42296  meaiuninclem  42304  meaiuninc3v  42308  isomenndlem  42354  ovnsubaddlem2  42395  hoidmvlelem3  42421  hoidmvlelem5  42423  hspdifhsp  42440  hoiqssbllem3  42448  hspmbllem2  42451  vonioo  42506  vonicc  42509  pimdecfgtioo  42537  issmflem  42546  issmfle  42564  issmfgt  42575  issmfgelem  42587  smflimlem2  42590  smfinflem  42633  smflimsuplem5  42640  smfliminflem  42646  sbgoldbm  43431  sbgoldbo  43434  aacllem  44382