Theorem rspa 3245

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

Assertion

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

Proof of Theorem rspa

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∀wral 3061

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 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-ral 3062

This theorem is referenced by:  r19.21bi  3248  dfiun2gOLD  5033  mpteq12f  5235  reusv2lem2  5396  frrlem12  8278  axdc4lem  10446  fprodle  15936  isucn2  23775  bcthlem5  24836  gausslemma2dlem6  26864  opreu2reuALT  31704  foresf1o  31729  abrexss  31736  iinabrex  31787  reff  32807  locfinreflem  32808  cmpcref  32818  zarclsiin  32839  ldgenpisyslem1  33149  voliune  33215  volfiniune  33216  reprpmtf1o  33626  bnj1366  33828  heicant  36511  indexdom  36590  glbconxN  38237  pmapglbx  38628  pmapglb2xN  38631  mzpexpmpt  41468  uzwo4  43725  ralimralim  43755  eliinid  43785  suprnmpt  43855  wessf1ornlem  43867  fompt  43875  disjinfi  43876  choicefi  43884  axccdom  43906  axccd  43913  rnmptlb  43932  rnmptbddlem  43933  rnmptbd2lem  43938  upbdrech  44001  ssfiunibd  44005  iuneqfzuzlem  44030  xrralrecnnle  44079  supxrunb3  44095  supxrleubrnmpt  44102  unb2ltle  44111  rexabslelem  44114  suprleubrnmpt  44118  uzublem  44126  infxrgelbrnmpt  44150  cvgcaule  44188  fprodcnlem  44301  limcrecl  44331  islpcn  44341  limsupre  44343  limcleqr  44346  0ellimcdiv  44351  limclner  44353  climinf2lem  44408  climinf3  44418  limsupmnflem  44422  limsupmnfuzlem  44428  limsupre3uzlem  44437  climisp  44448  climrescn  44450  climxrrelem  44451  climxrre  44452  climxlim2lem  44547  cncfshift  44576  cncfperiod  44581  cncfuni  44588  cncfioobd  44599  dvbdfbdioolem1  44630  dvnprodlem2  44649  stoweidlem28  44730  stoweidlem29  44731  stoweidlem31  44733  stoweidlem60  44762  stoweidlem62  44764  fourierdlem39  44848  fourierdlem68  44876  fourierdlem73  44881  fourierdlem77  44885  fourierdlem80  44888  fourierdlem83  44891  fourierdlem87  44895  fourierdlem94  44902  fourierdlem103  44911  fourierdlem104  44912  fourierdlem112  44920  fourierdlem113  44921  qndenserrnbllem  44996  dfsalgen2  45043  subsaliuncl  45060  sge0lefi  45100  sge0isum  45129  sge0reuzb  45150  iundjiun  45162  voliunsge0lem  45174  meaiuninclem  45182  meaiuninc3v  45186  isomenndlem  45232  ovnsubaddlem2  45273  hoidmvlelem3  45299  hoidmvlelem5  45301  hspdifhsp  45318  hoiqssbllem3  45326  hspmbllem2  45329  vonioo  45384  vonicc  45387  pimdecfgtioo  45419  issmflem  45429  issmfle  45447  issmfgt  45458  issmfgelem  45471  smflimlem2  45474  smfinflem  45519  smflimsuplem5  45526  smfliminflem  45532  fsupdm  45544  finfdm  45548  sbgoldbm  46438  sbgoldbo  46441  aacllem  47801