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

Theorem rspa 2824
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 2823 . 2  |-  ( A. x  e.  A  ph  ->  ( x  e.  A  ->  ph ) )
21imp 429 1  |-  ( ( A. x  e.  A  ph 
/\  x  e.  A
)  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1819   A.wral 2807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-12 1855
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1614  df-ral 2812
This theorem is referenced by:  ralbi  2988  mpteq12f  4533  reusv2lem2  4658  axdc4lem  8852  isucn2  20908  bcthlem5  21893  foresf1o  27531  abrexss  27538  reff  28003  locfinreflem  28004  cmpcref  28014  voliune  28374  volfiniune  28375  heicant  30254  indexdom  30430  mzpexpmpt  30882  suprnmpt  31654  upbdrech  31708  ssfiunibd  31712  fprodle  31807  limcrecl  31838  islpcn  31848  limsupre  31850  limcleqr  31853  0ellimcdiv  31858  limclner  31860  cncfshift  31879  cncfperiod  31884  cncfuni  31892  cncfioobd  31903  dvbdfbdioolem1  31928  dvnprodlem2  31947  stoweidlem28  32013  stoweidlem29  32014  stoweidlem31  32016  stoweidlem60  32045  stoweidlem62  32047  fourierdlem39  32131  fourierdlem68  32160  fourierdlem73  32165  fourierdlem77  32169  fourierdlem80  32172  fourierdlem83  32175  fourierdlem87  32179  fourierdlem94  32186  fourierdlem103  32195  fourierdlem104  32196  fourierdlem112  32204  fourierdlem113  32205  aacllem  33360  bnj1366  34031  glbconxN  35245  pmapglbx  35636  pmapglb2xN  35639
  Copyright terms: Public domain W3C validator