Theorem rspa 3135

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

Assertion

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

Proof of Theorem rspa

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  ∀wral 3070

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 1911  ax-6 1970  ax-7 2015  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3075

This theorem is referenced by:  r19.21bi  3137  ralrexbidOLD  3247  ralimda  3408  dfiun2g  4922  mpteq12f  5118  reusv2lem2  5271  axdc4lem  9920  fprodle  15403  isucn2  22985  bcthlem5  24033  gausslemma2dlem6  26060  opreu2reuALT  30351  foresf1o  30377  abrexss  30384  iinabrex  30435  reff  31314  locfinreflem  31315  cmpcref  31325  zarclsiin  31346  ldgenpisyslem1  31654  voliune  31720  volfiniune  31721  reprpmtf1o  32129  bnj1366  32333  frrlem12  33400  heicant  35398  indexdom  35478  glbconxN  36980  pmapglbx  37371  pmapglb2xN  37374  mzpexpmpt  40087  uzwo4  42088  ralimralim  42118  eliinid  42148  suprnmpt  42197  wessf1ornlem  42209  fompt  42217  disjinfi  42218  choicefi  42227  axccdom  42249  axccd  42257  rnmptlb  42276  rnmptbddlem  42277  rnmptbd2lem  42282  upbdrech  42333  ssfiunibd  42337  iuneqfzuzlem  42362  xrralrecnnle  42413  supxrunb3  42430  supxrleubrnmpt  42437  unb2ltle  42446  rexabslelem  42449  suprleubrnmpt  42453  uzublem  42461  infxrgelbrnmpt  42487  fprodcnlem  42635  limcrecl  42665  islpcn  42675  limsupre  42677  limcleqr  42680  0ellimcdiv  42685  limclner  42687  climinf2lem  42742  climinf3  42752  limsupmnflem  42756  limsupmnfuzlem  42762  limsupre3uzlem  42771  climisp  42782  climrescn  42784  climxrrelem  42785  climxrre  42786  climxlim2lem  42881  cncfshift  42910  cncfperiod  42915  cncfuni  42922  cncfioobd  42933  dvbdfbdioolem1  42964  dvnprodlem2  42983  stoweidlem28  43064  stoweidlem29  43065  stoweidlem31  43067  stoweidlem60  43096  stoweidlem62  43098  fourierdlem39  43182  fourierdlem68  43210  fourierdlem73  43215  fourierdlem77  43219  fourierdlem80  43222  fourierdlem83  43225  fourierdlem87  43229  fourierdlem94  43236  fourierdlem103  43245  fourierdlem104  43246  fourierdlem112  43254  fourierdlem113  43255  qndenserrnbllem  43330  dfsalgen2  43375  subsaliuncl  43392  sge0lefi  43431  sge0isum  43460  sge0reuzb  43481  iundjiun  43493  voliunsge0lem  43505  meaiuninclem  43513  meaiuninc3v  43517  isomenndlem  43563  ovnsubaddlem2  43604  hoidmvlelem3  43630  hoidmvlelem5  43632  hspdifhsp  43649  hoiqssbllem3  43657  hspmbllem2  43660  vonioo  43715  vonicc  43718  pimdecfgtioo  43746  issmflem  43755  issmfle  43773  issmfgt  43784  issmfgelem  43796  smflimlem2  43799  smfinflem  43842  smflimsuplem5  43849  smfliminflem  43855  sbgoldbm  44697  sbgoldbo  44700  aacllem  45793