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

Theorem rspa 2959
Description: Restricted specialization. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Assertion
Ref Expression
rspa ((∀𝑥𝐴 𝜑𝑥𝐴) → 𝜑)

Proof of Theorem rspa
StepHypRef Expression
1 rsp 2958 . 2 (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))
21imp 444 1 ((∀𝑥𝐴 𝜑𝑥𝐴) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-ral 2946
This theorem is referenced by:  ralbi  3097  mpteq12f  4764  reusv2lem2  4899  reusv2lem2OLD  4900  axdc4lem  9315  fprodle  14771  isucn2  22130  bcthlem5  23171  gausslemma2dlem6  25142  foresf1o  29469  abrexss  29476  reff  30034  locfinreflem  30035  cmpcref  30045  ldgenpisyslem1  30354  voliune  30420  volfiniune  30421  reprpmtf1o  30832  bnj1366  31026  heicant  33574  indexdom  33659  glbconxN  34982  pmapglbx  35373  pmapglb2xN  35376  mzpexpmpt  37625  uzwo4  39535  ralimralim  39567  eliinid  39608  ralimda  39640  suprnmpt  39669  wessf1ornlem  39685  fompt  39693  disjinfi  39694  choicefi  39706  axccdom  39730  axccd  39743  rnmptlb  39767  rnmptbddlem  39769  rnmptbd2lem  39777  upbdrech  39833  ssfiunibd  39837  iuneqfzuzlem  39863  xrralrecnnle  39915  supxrunb3  39936  supxrleubrnmpt  39945  unb2ltle  39955  rexabslelem  39958  suprleubrnmpt  39962  uzublem  39970  infxrgelbrnmpt  39996  fprodcnlem  40149  limcrecl  40179  islpcn  40189  limsupre  40191  limcleqr  40194  0ellimcdiv  40199  limclner  40201  climinf2lem  40256  climinf3  40266  limsupmnflem  40270  limsupmnfuzlem  40276  limsupre3uzlem  40285  climisp  40296  climrescn  40298  climxrrelem  40299  climxrre  40300  climxlim2lem  40389  cncfshift  40405  cncfperiod  40410  cncfuni  40417  cncfioobd  40428  dvbdfbdioolem1  40461  dvnprodlem2  40480  stoweidlem28  40563  stoweidlem29  40564  stoweidlem31  40566  stoweidlem60  40595  stoweidlem62  40597  fourierdlem39  40681  fourierdlem68  40709  fourierdlem73  40714  fourierdlem77  40718  fourierdlem80  40721  fourierdlem83  40724  fourierdlem87  40728  fourierdlem94  40735  fourierdlem103  40744  fourierdlem104  40745  fourierdlem112  40753  fourierdlem113  40754  qndenserrnbllem  40832  dfsalgen2  40877  subsaliuncl  40894  sge0lefi  40933  sge0isum  40962  sge0reuzb  40983  iundjiun  40995  voliunsge0lem  41007  meaiuninclem  41015  meaiuninc3v  41019  isomenndlem  41065  ovnsubaddlem2  41106  hoidmvlelem3  41132  hoidmvlelem5  41134  hspdifhsp  41151  hoiqssbllem3  41159  hspmbllem2  41162  vonioo  41217  vonicc  41220  pimdecfgtioo  41248  issmflem  41257  issmfle  41275  issmfgt  41286  issmfgelem  41298  smflimlem2  41301  smfinflem  41344  smflimsuplem5  41351  smfliminflem  41357  sbgoldbm  41997  sbgoldbo  42000  aacllem  42875
  Copyright terms: Public domain W3C validator