Theorem rspa 3227

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

Assertion

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

Proof of Theorem rspa

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-ral 3053

This theorem is referenced by:  r19.21bi  3230  mpteq12f  5171  reusv2lem2  5337  fompt  7065  frrlem12  8241  axdc4lem  10371  fprodle  15955  isucn2  24256  bcthlem5  25308  gausslemma2dlem6  27352  opreu2reuALT  32564  foresf1o  32592  abrexss  32600  iinabrex  32657  reff  34002  locfinreflem  34003  cmpcref  34013  zarclsiin  34034  ldgenpisyslem1  34326  voliune  34392  volfiniune  34393  reprpmtf1o  34789  bnj1366  34990  weiunfrlem  36665  heicant  37993  indexdom  38072  glbconxN  39841  pmapglbx  40232  pmapglb2xN  40235  mzpexpmpt  43194  uzwo4  45505  ralimralim  45533  eliinid  45562  suprnmpt  45625  wessf1ornlem  45636  disjinfi  45643  choicefi  45650  axccdom  45672  axccd  45679  rnmptlb  45693  rnmptbddlem  45694  rnmptbd2lem  45698  upbdrech  45759  ssfiunibd  45763  iuneqfzuzlem  45785  xrralrecnnle  45833  supxrunb3  45849  supxrleubrnmpt  45855  unb2ltle  45864  rexabslelem  45867  suprleubrnmpt  45871  uzublem  45879  infxrgelbrnmpt  45903  cvgcaule  45940  fprodcnlem  46050  limcrecl  46080  islpcn  46088  limsupre  46090  limcleqr  46093  0ellimcdiv  46098  limclner  46100  climinf2lem  46155  climinf3  46165  limsupmnflem  46169  limsupmnfuzlem  46175  limsupre3uzlem  46184  climisp  46195  climrescn  46197  climxrrelem  46198  climxrre  46199  climxlim2lem  46294  cncfshift  46323  cncfperiod  46328  cncfuni  46335  cncfioobd  46346  dvbdfbdioolem1  46377  dvnprodlem2  46396  stoweidlem28  46477  stoweidlem29  46478  stoweidlem31  46480  stoweidlem60  46509  stoweidlem62  46511  fourierdlem39  46595  fourierdlem68  46623  fourierdlem73  46628  fourierdlem77  46632  fourierdlem80  46635  fourierdlem83  46638  fourierdlem87  46642  fourierdlem94  46649  fourierdlem103  46658  fourierdlem104  46659  fourierdlem112  46667  fourierdlem113  46668  qndenserrnbllem  46743  dfsalgen2  46790  subsaliuncl  46807  sge0lefi  46847  sge0isum  46876  sge0reuzb  46897  iundjiun  46909  voliunsge0lem  46921  meaiuninclem  46929  meaiuninc3v  46933  isomenndlem  46979  ovnsubaddlem2  47020  hoidmvlelem3  47046  hoidmvlelem5  47048  hspdifhsp  47065  hoiqssbllem3  47073  hspmbllem2  47076  vonioo  47131  vonicc  47134  pimdecfgtioo  47166  issmflem  47176  issmfle  47194  issmfgt  47205  issmfgelem  47218  smflimlem2  47221  smfinflem  47266  smflimsuplem5  47273  smfliminflem  47279  fsupdm  47291  finfdm  47295  sbgoldbm  48275  sbgoldbo  48278  aacllem  50291