Theorem rspa 3218

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

Assertion

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

Proof of Theorem rspa

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3045

This theorem is referenced by:  r19.21bi  3221  mpteq12f  5177  reusv2lem2  5338  fompt  7052  frrlem12  8230  axdc4lem  10349  fprodle  15903  isucn2  24164  bcthlem5  25226  gausslemma2dlem6  27281  opreu2reuALT  32421  foresf1o  32448  abrexss  32456  iinabrex  32513  reff  33806  locfinreflem  33807  cmpcref  33817  zarclsiin  33838  ldgenpisyslem1  34130  voliune  34196  volfiniune  34197  reprpmtf1o  34594  bnj1366  34796  weiunfrlem  36438  heicant  37635  indexdom  37714  glbconxN  39357  pmapglbx  39748  pmapglb2xN  39751  mzpexpmpt  42718  uzwo4  45031  ralimralim  45059  eliinid  45089  suprnmpt  45152  wessf1ornlem  45163  disjinfi  45170  choicefi  45178  axccdom  45200  axccd  45207  rnmptlb  45221  rnmptbddlem  45222  rnmptbd2lem  45226  upbdrech  45287  ssfiunibd  45291  iuneqfzuzlem  45314  xrralrecnnle  45362  supxrunb3  45378  supxrleubrnmpt  45385  unb2ltle  45394  rexabslelem  45397  suprleubrnmpt  45401  uzublem  45409  infxrgelbrnmpt  45433  cvgcaule  45470  fprodcnlem  45580  limcrecl  45610  islpcn  45620  limsupre  45622  limcleqr  45625  0ellimcdiv  45630  limclner  45632  climinf2lem  45687  climinf3  45697  limsupmnflem  45701  limsupmnfuzlem  45707  limsupre3uzlem  45716  climisp  45727  climrescn  45729  climxrrelem  45730  climxrre  45731  climxlim2lem  45826  cncfshift  45855  cncfperiod  45860  cncfuni  45867  cncfioobd  45878  dvbdfbdioolem1  45909  dvnprodlem2  45928  stoweidlem28  46009  stoweidlem29  46010  stoweidlem31  46012  stoweidlem60  46041  stoweidlem62  46043  fourierdlem39  46127  fourierdlem68  46155  fourierdlem73  46160  fourierdlem77  46164  fourierdlem80  46167  fourierdlem83  46170  fourierdlem87  46174  fourierdlem94  46181  fourierdlem103  46190  fourierdlem104  46191  fourierdlem112  46199  fourierdlem113  46200  qndenserrnbllem  46275  dfsalgen2  46322  subsaliuncl  46339  sge0lefi  46379  sge0isum  46408  sge0reuzb  46429  iundjiun  46441  voliunsge0lem  46453  meaiuninclem  46461  meaiuninc3v  46465  isomenndlem  46511  ovnsubaddlem2  46552  hoidmvlelem3  46578  hoidmvlelem5  46580  hspdifhsp  46597  hoiqssbllem3  46605  hspmbllem2  46608  vonioo  46663  vonicc  46666  pimdecfgtioo  46698  issmflem  46708  issmfle  46726  issmfgt  46737  issmfgelem  46750  smflimlem2  46753  smfinflem  46798  smflimsuplem5  46805  smfliminflem  46811  fsupdm  46823  finfdm  46827  sbgoldbm  47768  sbgoldbo  47771  aacllem  49786