Theorem rspa 3225

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

Assertion

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

Proof of Theorem rspa

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2184

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3052

This theorem is referenced by:  r19.21bi  3228  mpteq12f  5183  reusv2lem2  5344  fompt  7063  frrlem12  8239  axdc4lem  10365  fprodle  15919  isucn2  24222  bcthlem5  25284  gausslemma2dlem6  27339  opreu2reuALT  32551  foresf1o  32579  abrexss  32587  iinabrex  32644  reff  33996  locfinreflem  33997  cmpcref  34007  zarclsiin  34028  ldgenpisyslem1  34320  voliune  34386  volfiniune  34387  reprpmtf1o  34783  bnj1366  34985  weiunfrlem  36658  heicant  37856  indexdom  37935  glbconxN  39638  pmapglbx  40029  pmapglb2xN  40032  mzpexpmpt  42987  uzwo4  45298  ralimralim  45326  eliinid  45355  suprnmpt  45418  wessf1ornlem  45429  disjinfi  45436  choicefi  45444  axccdom  45466  axccd  45473  rnmptlb  45487  rnmptbddlem  45488  rnmptbd2lem  45492  upbdrech  45553  ssfiunibd  45557  iuneqfzuzlem  45579  xrralrecnnle  45627  supxrunb3  45643  supxrleubrnmpt  45650  unb2ltle  45659  rexabslelem  45662  suprleubrnmpt  45666  uzublem  45674  infxrgelbrnmpt  45698  cvgcaule  45735  fprodcnlem  45845  limcrecl  45875  islpcn  45883  limsupre  45885  limcleqr  45888  0ellimcdiv  45893  limclner  45895  climinf2lem  45950  climinf3  45960  limsupmnflem  45964  limsupmnfuzlem  45970  limsupre3uzlem  45979  climisp  45990  climrescn  45992  climxrrelem  45993  climxrre  45994  climxlim2lem  46089  cncfshift  46118  cncfperiod  46123  cncfuni  46130  cncfioobd  46141  dvbdfbdioolem1  46172  dvnprodlem2  46191  stoweidlem28  46272  stoweidlem29  46273  stoweidlem31  46275  stoweidlem60  46304  stoweidlem62  46306  fourierdlem39  46390  fourierdlem68  46418  fourierdlem73  46423  fourierdlem77  46427  fourierdlem80  46430  fourierdlem83  46433  fourierdlem87  46437  fourierdlem94  46444  fourierdlem103  46453  fourierdlem104  46454  fourierdlem112  46462  fourierdlem113  46463  qndenserrnbllem  46538  dfsalgen2  46585  subsaliuncl  46602  sge0lefi  46642  sge0isum  46671  sge0reuzb  46692  iundjiun  46704  voliunsge0lem  46716  meaiuninclem  46724  meaiuninc3v  46728  isomenndlem  46774  ovnsubaddlem2  46815  hoidmvlelem3  46841  hoidmvlelem5  46843  hspdifhsp  46860  hoiqssbllem3  46868  hspmbllem2  46871  vonioo  46926  vonicc  46929  pimdecfgtioo  46961  issmflem  46971  issmfle  46989  issmfgt  47000  issmfgelem  47013  smflimlem2  47016  smfinflem  47061  smflimsuplem5  47068  smfliminflem  47074  fsupdm  47086  finfdm  47090  sbgoldbm  48030  sbgoldbo  48033  aacllem  50046