Theorem rspa 3254

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

Assertion

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

Proof of Theorem rspa

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-ral 3068

This theorem is referenced by:  r19.21bi  3257  dfiun2gOLD  5054  mpteq12f  5254  reusv2lem2  5417  fompt  7152  frrlem12  8338  axdc4lem  10524  fprodle  16044  isucn2  24309  bcthlem5  25381  gausslemma2dlem6  27434  opreu2reuALT  32505  foresf1o  32532  abrexss  32540  iinabrex  32591  reff  33785  locfinreflem  33786  cmpcref  33796  zarclsiin  33817  ldgenpisyslem1  34127  voliune  34193  volfiniune  34194  reprpmtf1o  34603  bnj1366  34805  weiunfrlem  36430  heicant  37615  indexdom  37694  glbconxN  39335  pmapglbx  39726  pmapglb2xN  39729  mzpexpmpt  42701  uzwo4  44955  ralimralim  44983  eliinid  45013  suprnmpt  45081  wessf1ornlem  45092  disjinfi  45099  choicefi  45107  axccdom  45129  axccd  45136  rnmptlb  45152  rnmptbddlem  45153  rnmptbd2lem  45157  upbdrech  45220  ssfiunibd  45224  iuneqfzuzlem  45249  xrralrecnnle  45298  supxrunb3  45314  supxrleubrnmpt  45321  unb2ltle  45330  rexabslelem  45333  suprleubrnmpt  45337  uzublem  45345  infxrgelbrnmpt  45369  cvgcaule  45407  fprodcnlem  45520  limcrecl  45550  islpcn  45560  limsupre  45562  limcleqr  45565  0ellimcdiv  45570  limclner  45572  climinf2lem  45627  climinf3  45637  limsupmnflem  45641  limsupmnfuzlem  45647  limsupre3uzlem  45656  climisp  45667  climrescn  45669  climxrrelem  45670  climxrre  45671  climxlim2lem  45766  cncfshift  45795  cncfperiod  45800  cncfuni  45807  cncfioobd  45818  dvbdfbdioolem1  45849  dvnprodlem2  45868  stoweidlem28  45949  stoweidlem29  45950  stoweidlem31  45952  stoweidlem60  45981  stoweidlem62  45983  fourierdlem39  46067  fourierdlem68  46095  fourierdlem73  46100  fourierdlem77  46104  fourierdlem80  46107  fourierdlem83  46110  fourierdlem87  46114  fourierdlem94  46121  fourierdlem103  46130  fourierdlem104  46131  fourierdlem112  46139  fourierdlem113  46140  qndenserrnbllem  46215  dfsalgen2  46262  subsaliuncl  46279  sge0lefi  46319  sge0isum  46348  sge0reuzb  46369  iundjiun  46381  voliunsge0lem  46393  meaiuninclem  46401  meaiuninc3v  46405  isomenndlem  46451  ovnsubaddlem2  46492  hoidmvlelem3  46518  hoidmvlelem5  46520  hspdifhsp  46537  hoiqssbllem3  46545  hspmbllem2  46548  vonioo  46603  vonicc  46606  pimdecfgtioo  46638  issmflem  46648  issmfle  46666  issmfgt  46677  issmfgelem  46690  smflimlem2  46693  smfinflem  46738  smflimsuplem5  46745  smfliminflem  46751  fsupdm  46763  finfdm  46767  sbgoldbm  47658  sbgoldbo  47661  aacllem  48895