Theorem rspa 3240

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

Assertion

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

Proof of Theorem rspa

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2099  ∀wral 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-12 2164

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-ral 3057

This theorem is referenced by:  r19.21bi  3243  dfiun2gOLD  5028  mpteq12f  5230  reusv2lem2  5393  fompt  7122  frrlem12  8296  axdc4lem  10472  fprodle  15966  isucn2  24177  bcthlem5  25249  gausslemma2dlem6  27298  opreu2reuALT  32268  foresf1o  32293  abrexss  32300  iinabrex  32352  reff  33430  locfinreflem  33431  cmpcref  33441  zarclsiin  33462  ldgenpisyslem1  33772  voliune  33838  volfiniune  33839  reprpmtf1o  34248  bnj1366  34450  heicant  37117  indexdom  37196  glbconxN  38840  pmapglbx  39231  pmapglb2xN  39234  mzpexpmpt  42137  uzwo4  44389  ralimralim  44419  eliinid  44449  suprnmpt  44519  wessf1ornlem  44530  disjinfi  44537  choicefi  44545  axccdom  44567  axccd  44574  rnmptlb  44591  rnmptbddlem  44592  rnmptbd2lem  44596  upbdrech  44659  ssfiunibd  44663  iuneqfzuzlem  44688  xrralrecnnle  44737  supxrunb3  44753  supxrleubrnmpt  44760  unb2ltle  44769  rexabslelem  44772  suprleubrnmpt  44776  uzublem  44784  infxrgelbrnmpt  44808  cvgcaule  44846  fprodcnlem  44959  limcrecl  44989  islpcn  44999  limsupre  45001  limcleqr  45004  0ellimcdiv  45009  limclner  45011  climinf2lem  45066  climinf3  45076  limsupmnflem  45080  limsupmnfuzlem  45086  limsupre3uzlem  45095  climisp  45106  climrescn  45108  climxrrelem  45109  climxrre  45110  climxlim2lem  45205  cncfshift  45234  cncfperiod  45239  cncfuni  45246  cncfioobd  45257  dvbdfbdioolem1  45288  dvnprodlem2  45307  stoweidlem28  45388  stoweidlem29  45389  stoweidlem31  45391  stoweidlem60  45420  stoweidlem62  45422  fourierdlem39  45506  fourierdlem68  45534  fourierdlem73  45539  fourierdlem77  45543  fourierdlem80  45546  fourierdlem83  45549  fourierdlem87  45553  fourierdlem94  45560  fourierdlem103  45569  fourierdlem104  45570  fourierdlem112  45578  fourierdlem113  45579  qndenserrnbllem  45654  dfsalgen2  45701  subsaliuncl  45718  sge0lefi  45758  sge0isum  45787  sge0reuzb  45808  iundjiun  45820  voliunsge0lem  45832  meaiuninclem  45840  meaiuninc3v  45844  isomenndlem  45890  ovnsubaddlem2  45931  hoidmvlelem3  45957  hoidmvlelem5  45959  hspdifhsp  45976  hoiqssbllem3  45984  hspmbllem2  45987  vonioo  46042  vonicc  46045  pimdecfgtioo  46077  issmflem  46087  issmfle  46105  issmfgt  46116  issmfgelem  46129  smflimlem2  46132  smfinflem  46177  smflimsuplem5  46184  smfliminflem  46190  fsupdm  46202  finfdm  46206  sbgoldbm  47096  sbgoldbo  47099  aacllem  48206