Theorem rspa 3246

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

Assertion

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

Proof of Theorem rspa

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-ral 3063

This theorem is referenced by:  r19.21bi  3249  dfiun2gOLD  5035  mpteq12f  5237  reusv2lem2  5398  frrlem12  8282  axdc4lem  10450  fprodle  15940  isucn2  23784  bcthlem5  24845  gausslemma2dlem6  26875  opreu2reuALT  31717  foresf1o  31742  abrexss  31749  iinabrex  31800  reff  32819  locfinreflem  32820  cmpcref  32830  zarclsiin  32851  ldgenpisyslem1  33161  voliune  33227  volfiniune  33228  reprpmtf1o  33638  bnj1366  33840  heicant  36523  indexdom  36602  glbconxN  38249  pmapglbx  38640  pmapglb2xN  38643  mzpexpmpt  41483  uzwo4  43740  ralimralim  43770  eliinid  43800  suprnmpt  43870  wessf1ornlem  43882  fompt  43890  disjinfi  43891  choicefi  43899  axccdom  43921  axccd  43928  rnmptlb  43947  rnmptbddlem  43948  rnmptbd2lem  43952  upbdrech  44015  ssfiunibd  44019  iuneqfzuzlem  44044  xrralrecnnle  44093  supxrunb3  44109  supxrleubrnmpt  44116  unb2ltle  44125  rexabslelem  44128  suprleubrnmpt  44132  uzublem  44140  infxrgelbrnmpt  44164  cvgcaule  44202  fprodcnlem  44315  limcrecl  44345  islpcn  44355  limsupre  44357  limcleqr  44360  0ellimcdiv  44365  limclner  44367  climinf2lem  44422  climinf3  44432  limsupmnflem  44436  limsupmnfuzlem  44442  limsupre3uzlem  44451  climisp  44462  climrescn  44464  climxrrelem  44465  climxrre  44466  climxlim2lem  44561  cncfshift  44590  cncfperiod  44595  cncfuni  44602  cncfioobd  44613  dvbdfbdioolem1  44644  dvnprodlem2  44663  stoweidlem28  44744  stoweidlem29  44745  stoweidlem31  44747  stoweidlem60  44776  stoweidlem62  44778  fourierdlem39  44862  fourierdlem68  44890  fourierdlem73  44895  fourierdlem77  44899  fourierdlem80  44902  fourierdlem83  44905  fourierdlem87  44909  fourierdlem94  44916  fourierdlem103  44925  fourierdlem104  44926  fourierdlem112  44934  fourierdlem113  44935  qndenserrnbllem  45010  dfsalgen2  45057  subsaliuncl  45074  sge0lefi  45114  sge0isum  45143  sge0reuzb  45164  iundjiun  45176  voliunsge0lem  45188  meaiuninclem  45196  meaiuninc3v  45200  isomenndlem  45246  ovnsubaddlem2  45287  hoidmvlelem3  45313  hoidmvlelem5  45315  hspdifhsp  45332  hoiqssbllem3  45340  hspmbllem2  45343  vonioo  45398  vonicc  45401  pimdecfgtioo  45433  issmflem  45443  issmfle  45461  issmfgt  45472  issmfgelem  45485  smflimlem2  45488  smfinflem  45533  smflimsuplem5  45540  smfliminflem  45546  fsupdm  45558  finfdm  45562  sbgoldbm  46452  sbgoldbo  46455  aacllem  47848