Theorem rspa 2930

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

Assertion

Ref	Expression
rspa	|- ( ( A. x e. A ph /\ x e. A ) -> ph )

Proof of Theorem rspa

Step	Hyp	Ref	Expression
1		rsp 2929	. 2 |- ( A. x e. A ph -> ( x e. A -> ph ) )
2	1	imp 445	1 |- ( ( A. x e. A ph /\ x e. A ) -> ph )

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   A.wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917

This theorem is referenced by:  ralbi  3068  mpteq12f  4731  reusv2lem2  4869  reusv2lem2OLD  4870  axdc4lem  9277  fprodle  14727  isucn2  22083  bcthlem5  23125  gausslemma2dlem6  25097  foresf1o  29343  abrexss  29350  reff  29906  locfinreflem  29907  cmpcref  29917  ldgenpisyslem1  30226  voliune  30292  volfiniune  30293  reprpmtf1o  30704  bnj1366  30900  heicant  33444  indexdom  33529  glbconxN  34664  pmapglbx  35055  pmapglb2xN  35058  mzpexpmpt  37308  uzwo4  39221  ralimralim  39253  eliinid  39294  ralimda  39326  suprnmpt  39355  wessf1ornlem  39371  fompt  39379  disjinfi  39380  choicefi  39392  axccdom  39416  axccd  39429  rnmptlb  39453  rnmptbddlem  39455  rnmptbd2lem  39463  upbdrech  39519  ssfiunibd  39523  iuneqfzuzlem  39550  xrralrecnnle  39602  supxrunb3  39623  supxrleubrnmpt  39632  unb2ltle  39642  rexabslelem  39645  suprleubrnmpt  39649  uzublem  39657  infxrgelbrnmpt  39683  fprodcnlem  39831  limcrecl  39861  islpcn  39871  limsupre  39873  limcleqr  39876  0ellimcdiv  39881  limclner  39883  climinf2lem  39938  climinf3  39948  limsupmnflem  39952  limsupmnfuzlem  39958  limsupre3uzlem  39967  climisp  39978  climrescn  39980  climxrrelem  39981  climxrre  39982  climxlim2lem  40071  cncfshift  40087  cncfperiod  40092  cncfuni  40099  cncfioobd  40110  dvbdfbdioolem1  40143  dvnprodlem2  40162  stoweidlem28  40245  stoweidlem29  40246  stoweidlem31  40248  stoweidlem60  40277  stoweidlem62  40279  fourierdlem39  40363  fourierdlem68  40391  fourierdlem73  40396  fourierdlem77  40400  fourierdlem80  40403  fourierdlem83  40406  fourierdlem87  40410  fourierdlem94  40417  fourierdlem103  40426  fourierdlem104  40427  fourierdlem112  40435  fourierdlem113  40436  qndenserrnbllem  40514  dfsalgen2  40559  subsaliuncl  40576  sge0lefi  40615  sge0isum  40644  sge0reuzb  40665  iundjiun  40677  voliunsge0lem  40689  meaiuninclem  40697  isomenndlem  40744  ovnsubaddlem2  40785  hoidmvlelem3  40811  hoidmvlelem5  40813  hspdifhsp  40830  hoiqssbllem3  40838  hspmbllem2  40841  vonioo  40896  vonicc  40899  pimdecfgtioo  40927  issmflem  40936  issmfle  40954  issmfgt  40965  issmfgelem  40977  smflimlem2  40980  smfinflem  41023  smflimsuplem5  41030  smfliminflem  41036  sbgoldbm  41672  sbgoldbo  41675  aacllem  42547