Theorem rspa 3245

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

Assertion

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

Proof of Theorem rspa

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-12 2174

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-ral 3059

This theorem is referenced by:  r19.21bi  3248  dfiun2gOLD  5035  mpteq12f  5235  reusv2lem2  5404  fompt  7137  frrlem12  8320  axdc4lem  10492  fprodle  16028  isucn2  24303  bcthlem5  25375  gausslemma2dlem6  27430  opreu2reuALT  32504  foresf1o  32531  abrexss  32539  iinabrex  32588  reff  33799  locfinreflem  33800  cmpcref  33810  zarclsiin  33831  ldgenpisyslem1  34143  voliune  34209  volfiniune  34210  reprpmtf1o  34619  bnj1366  34821  weiunfrlem  36446  heicant  37641  indexdom  37720  glbconxN  39360  pmapglbx  39751  pmapglb2xN  39754  mzpexpmpt  42732  uzwo4  44992  ralimralim  45020  eliinid  45050  suprnmpt  45116  wessf1ornlem  45127  disjinfi  45134  choicefi  45142  axccdom  45164  axccd  45171  rnmptlb  45187  rnmptbddlem  45188  rnmptbd2lem  45192  upbdrech  45255  ssfiunibd  45259  iuneqfzuzlem  45283  xrralrecnnle  45332  supxrunb3  45348  supxrleubrnmpt  45355  unb2ltle  45364  rexabslelem  45367  suprleubrnmpt  45371  uzublem  45379  infxrgelbrnmpt  45403  cvgcaule  45441  fprodcnlem  45554  limcrecl  45584  islpcn  45594  limsupre  45596  limcleqr  45599  0ellimcdiv  45604  limclner  45606  climinf2lem  45661  climinf3  45671  limsupmnflem  45675  limsupmnfuzlem  45681  limsupre3uzlem  45690  climisp  45701  climrescn  45703  climxrrelem  45704  climxrre  45705  climxlim2lem  45800  cncfshift  45829  cncfperiod  45834  cncfuni  45841  cncfioobd  45852  dvbdfbdioolem1  45883  dvnprodlem2  45902  stoweidlem28  45983  stoweidlem29  45984  stoweidlem31  45986  stoweidlem60  46015  stoweidlem62  46017  fourierdlem39  46101  fourierdlem68  46129  fourierdlem73  46134  fourierdlem77  46138  fourierdlem80  46141  fourierdlem83  46144  fourierdlem87  46148  fourierdlem94  46155  fourierdlem103  46164  fourierdlem104  46165  fourierdlem112  46173  fourierdlem113  46174  qndenserrnbllem  46249  dfsalgen2  46296  subsaliuncl  46313  sge0lefi  46353  sge0isum  46382  sge0reuzb  46403  iundjiun  46415  voliunsge0lem  46427  meaiuninclem  46435  meaiuninc3v  46439  isomenndlem  46485  ovnsubaddlem2  46526  hoidmvlelem3  46552  hoidmvlelem5  46554  hspdifhsp  46571  hoiqssbllem3  46579  hspmbllem2  46582  vonioo  46637  vonicc  46640  pimdecfgtioo  46672  issmflem  46682  issmfle  46700  issmfgt  46711  issmfgelem  46724  smflimlem2  46727  smfinflem  46772  smflimsuplem5  46779  smfliminflem  46785  fsupdm  46797  finfdm  46801  sbgoldbm  47708  sbgoldbo  47711  aacllem  49031