Theorem rspa 3251

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

Assertion

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

Proof of Theorem rspa

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2142  ∀wral 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-12 2212

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-ral 3077

This theorem is referenced by:  r19.21bi  3254  mpteq12f  5185  reusv2lem2  5356  fompt  7099  frrlem12  8278  axdc4lem  10412  fprodle  16026  isucn2  24338  bcthlem5  25390  gausslemma2dlem6  27436  opreu2reuALT  32676  foresf1o  32703  abrexss  32711  iinabrex  32769  reff  34136  locfinreflem  34137  cmpcref  34147  zarclsiin  34168  ldgenpisyslem1  34460  voliune  34526  volfiniune  34527  reprpmtf1o  34920  bnj1366  35124  weiunfrlem  36824  heicant  38154  indexdom  38233  glbconxN  40002  pmapglbx  40393  pmapglb2xN  40396  mzpexpmpt  43326  uzwo4  45633  ralimralim  45661  eliinid  45689  suprnmpt  45752  wessf1ornlem  45763  disjinfi  45770  choicefi  45777  axccdom  45798  axccd  45804  rnmptlb  45818  rnmptbddlem  45819  rnmptbd2lem  45823  upbdrech  45884  ssfiunibd  45888  iuneqfzuzlem  45910  xrralrecnnle  45958  supxrunb3  45974  supxrleubrnmpt  45980  unb2ltle  45989  rexabslelem  45992  suprleubrnmpt  45996  uzublem  46004  infxrgelbrnmpt  46028  cvgcaule  46065  fprodcnlem  46175  limcrecl  46205  islpcn  46213  limsupre  46215  limcleqr  46218  0ellimcdiv  46223  limclner  46225  climinf2lem  46280  climinf3  46290  limsupmnflem  46294  limsupmnfuzlem  46300  limsupre3uzlem  46309  climisp  46320  climrescn  46322  climxrrelem  46323  climxrre  46324  climxlim2lem  46419  cncfshift  46448  cncfperiod  46453  cncfuni  46460  cncfioobd  46471  dvbdfbdioolem1  46502  dvnprodlem2  46521  stoweidlem28  46602  stoweidlem29  46603  stoweidlem31  46605  stoweidlem60  46634  stoweidlem62  46636  fourierdlem39  46720  fourierdlem68  46748  fourierdlem73  46753  fourierdlem77  46757  fourierdlem80  46760  fourierdlem83  46763  fourierdlem87  46767  fourierdlem94  46774  fourierdlem103  46783  fourierdlem104  46784  fourierdlem112  46792  fourierdlem113  46793  qndenserrnbllem  46868  dfsalgen2  46915  subsaliuncl  46932  sge0lefi  46972  sge0isum  47001  sge0reuzb  47022  iundjiun  47034  voliunsge0lem  47046  meaiuninclem  47054  meaiuninc3v  47058  isomenndlem  47104  ovnsubaddlem2  47145  hoidmvlelem3  47171  hoidmvlelem5  47173  hspdifhsp  47190  hoiqssbllem3  47198  hspmbllem2  47201  vonioo  47256  vonicc  47259  pimdecfgtioo  47291  issmflem  47301  issmfle  47319  issmfgt  47330  issmfgelem  47343  smflimlem2  47346  smfinflem  47391  smflimsuplem5  47398  smfliminflem  47404  fsupdm  47416  finfdm  47420  sbgoldbm  48406  sbgoldbo  48409  aacllem  50422