MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rspa Structured version   Visualization version   Unicode version

Theorem rspa 2767
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
StepHypRef Expression
1 rsp 2766 . 2  |-  ( A. x  e.  A  ph  ->  ( x  e.  A  ->  ph ) )
21imp 435 1  |-  ( ( A. x  e.  A  ph 
/\  x  e.  A
)  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    e. wcel 1898   A.wral 2749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-12 1944
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-ral 2754
This theorem is referenced by:  ralbi  2933  mpteq12f  4493  reusv2lem2  4619  axdc4lem  8911  fprodle  14099  isucn2  21343  bcthlem5  22345  foresf1o  28188  abrexss  28195  reff  28715  locfinreflem  28716  cmpcref  28726  ldgenpisyslem1  29034  voliune  29101  volfiniune  29102  bnj1366  29690  heicant  32020  indexdom  32106  glbconxN  32988  pmapglbx  33379  pmapglb2xN  33382  mzpexpmpt  35632  uzwo4  37430  suprnmpt  37477  wessf1ornlem  37497  fompt  37505  disjinfi  37506  fvixp2  37516  choicefi  37519  upbdrech  37561  ssfiunibd  37565  iuneqfzuzlem  37595  limcrecl  37747  islpcn  37757  limsupre  37759  limsupreOLD  37760  limcleqr  37763  0ellimcdiv  37768  limclner  37770  cncfshift  37789  cncfperiod  37794  cncfuni  37802  cncfioobd  37813  dvbdfbdioolem1  37838  dvnprodlem2  37860  stoweidlem28  37926  stoweidlem29  37927  stoweidlem29OLD  37928  stoweidlem31  37930  stoweidlem60  37959  stoweidlem62  37961  stoweidlem62OLD  37962  fourierdlem39  38047  fourierdlem68  38076  fourierdlem73  38081  fourierdlem77  38085  fourierdlem80  38088  fourierdlem83  38091  fourierdlem87  38095  fourierdlem94  38102  fourierdlem103  38111  fourierdlem104  38112  fourierdlem112  38120  fourierdlem113  38121  qndenserrnbllem  38201  dfsalgen2  38238  sge0lefi  38278  sge0isum  38307  iundjiun  38336  isomenndlem  38389  ovnsubaddlem2  38431  hoidmvlelem3  38457  hoidmvlelem5  38459  hspdifhsp  38476  hoiqssbllem3  38484  hspmbllem2  38487  aacllem  40813
  Copyright terms: Public domain W3C validator