Theorem rspa 3248

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

Assertion

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

Proof of Theorem rspa

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3062

This theorem is referenced by:  r19.21bi  3251  dfiun2gOLD  5031  mpteq12f  5230  reusv2lem2  5399  fompt  7138  frrlem12  8322  axdc4lem  10495  fprodle  16032  isucn2  24288  bcthlem5  25362  gausslemma2dlem6  27416  opreu2reuALT  32496  foresf1o  32523  abrexss  32531  iinabrex  32582  reff  33838  locfinreflem  33839  cmpcref  33849  zarclsiin  33870  ldgenpisyslem1  34164  voliune  34230  volfiniune  34231  reprpmtf1o  34641  bnj1366  34843  weiunfrlem  36465  heicant  37662  indexdom  37741  glbconxN  39380  pmapglbx  39771  pmapglb2xN  39774  mzpexpmpt  42756  uzwo4  45058  ralimralim  45086  eliinid  45116  suprnmpt  45179  wessf1ornlem  45190  disjinfi  45197  choicefi  45205  axccdom  45227  axccd  45234  rnmptlb  45250  rnmptbddlem  45251  rnmptbd2lem  45255  upbdrech  45317  ssfiunibd  45321  iuneqfzuzlem  45345  xrralrecnnle  45394  supxrunb3  45410  supxrleubrnmpt  45417  unb2ltle  45426  rexabslelem  45429  suprleubrnmpt  45433  uzublem  45441  infxrgelbrnmpt  45465  cvgcaule  45502  fprodcnlem  45614  limcrecl  45644  islpcn  45654  limsupre  45656  limcleqr  45659  0ellimcdiv  45664  limclner  45666  climinf2lem  45721  climinf3  45731  limsupmnflem  45735  limsupmnfuzlem  45741  limsupre3uzlem  45750  climisp  45761  climrescn  45763  climxrrelem  45764  climxrre  45765  climxlim2lem  45860  cncfshift  45889  cncfperiod  45894  cncfuni  45901  cncfioobd  45912  dvbdfbdioolem1  45943  dvnprodlem2  45962  stoweidlem28  46043  stoweidlem29  46044  stoweidlem31  46046  stoweidlem60  46075  stoweidlem62  46077  fourierdlem39  46161  fourierdlem68  46189  fourierdlem73  46194  fourierdlem77  46198  fourierdlem80  46201  fourierdlem83  46204  fourierdlem87  46208  fourierdlem94  46215  fourierdlem103  46224  fourierdlem104  46225  fourierdlem112  46233  fourierdlem113  46234  qndenserrnbllem  46309  dfsalgen2  46356  subsaliuncl  46373  sge0lefi  46413  sge0isum  46442  sge0reuzb  46463  iundjiun  46475  voliunsge0lem  46487  meaiuninclem  46495  meaiuninc3v  46499  isomenndlem  46545  ovnsubaddlem2  46586  hoidmvlelem3  46612  hoidmvlelem5  46614  hspdifhsp  46631  hoiqssbllem3  46639  hspmbllem2  46642  vonioo  46697  vonicc  46700  pimdecfgtioo  46732  issmflem  46742  issmfle  46760  issmfgt  46771  issmfgelem  46784  smflimlem2  46787  smfinflem  46832  smflimsuplem5  46839  smfliminflem  46845  fsupdm  46857  finfdm  46861  sbgoldbm  47771  sbgoldbo  47774  aacllem  49320