Theorem rspa 3260

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

Assertion

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

Proof of Theorem rspa

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-ral 3086

This theorem is referenced by:  r19.21bi  3263  mpteq12f  5200  reusv2lem2  5371  fompt  7114  frrlem12  8293  axdc4lem  10438  fprodle  16049  isucn2  24403  bcthlem5  25455  gausslemma2dlem6  27501  opreu2reuALT  32763  foresf1o  32790  abrexss  32798  iinabrex  32854  reff  34173  locfinreflem  34174  cmpcref  34184  zarclsiin  34205  ldgenpisyslem1  34497  voliune  34563  volfiniune  34564  reprpmtf1o  34957  bnj1366  35161  weiunfrlem  36863  heicant  38193  indexdom  38272  glbconxN  40041  pmapglbx  40432  pmapglb2xN  40435  mzpexpmpt  43367  uzwo4  45664  ralimralim  45692  eliinid  45720  suprnmpt  45783  wessf1ornlem  45794  disjinfi  45801  choicefi  45808  axccdom  45829  axccd  45835  rnmptlb  45849  rnmptbddlem  45850  rnmptbd2lem  45854  upbdrech  45915  ssfiunibd  45919  iuneqfzuzlem  45941  xrralrecnnle  45989  supxrunb3  46005  supxrleubrnmpt  46011  unb2ltle  46020  rexabslelem  46023  suprleubrnmpt  46027  uzublem  46035  infxrgelbrnmpt  46059  cvgcaule  46096  fprodcnlem  46206  limcrecl  46236  islpcn  46244  limsupre  46246  limcleqr  46249  0ellimcdiv  46254  limclner  46256  climinf2lem  46311  climinf3  46321  limsupmnflem  46325  limsupmnfuzlem  46331  limsupre3uzlem  46340  climisp  46351  climrescn  46353  climxrrelem  46354  climxrre  46355  climxlim2lem  46450  cncfshift  46479  cncfperiod  46484  cncfuni  46491  cncfioobd  46502  dvbdfbdioolem1  46533  dvnprodlem2  46552  stoweidlem28  46633  stoweidlem29  46634  stoweidlem31  46636  stoweidlem60  46665  stoweidlem62  46667  fourierdlem39  46751  fourierdlem68  46779  fourierdlem73  46784  fourierdlem77  46788  fourierdlem80  46791  fourierdlem83  46794  fourierdlem87  46798  fourierdlem94  46805  fourierdlem103  46814  fourierdlem104  46815  fourierdlem112  46823  fourierdlem113  46824  qndenserrnbllem  46899  dfsalgen2  46946  subsaliuncl  46963  sge0lefi  47003  sge0isum  47032  sge0reuzb  47053  iundjiun  47065  voliunsge0lem  47077  meaiuninclem  47085  meaiuninc3v  47089  isomenndlem  47135  ovnsubaddlem2  47176  hoidmvlelem3  47202  hoidmvlelem5  47204  hspdifhsp  47221  hoiqssbllem3  47229  hspmbllem2  47232  vonioo  47287  vonicc  47290  pimdecfgtioo  47322  issmflem  47332  issmfle  47350  issmfgt  47361  issmfgelem  47374  smflimlem2  47377  smfinflem  47422  smflimsuplem5  47429  smfliminflem  47435  fsupdm  47447  finfdm  47451  sbgoldbm  48437  sbgoldbo  48440  aacllem  50474