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

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

Proof of Theorem rspa
StepHypRef Expression
1 rsp 3229 . 2 (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))
21imp 408 1 ((∀𝑥𝐴 𝜑𝑥𝐴) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-ral 3062
This theorem is referenced by:  r19.21bi  3233  dfiun2gOLD  4992  mpteq12f  5194  reusv2lem2  5355  frrlem12  8229  axdc4lem  10396  fprodle  15884  isucn2  23647  bcthlem5  24708  gausslemma2dlem6  26736  opreu2reuALT  31448  foresf1o  31474  abrexss  31481  iinabrex  31533  reff  32477  locfinreflem  32478  cmpcref  32488  zarclsiin  32509  ldgenpisyslem1  32819  voliune  32885  volfiniune  32886  reprpmtf1o  33296  bnj1366  33498  heicant  36159  indexdom  36239  glbconxN  37887  pmapglbx  38278  pmapglb2xN  38281  mzpexpmpt  41111  uzwo4  43349  ralimralim  43379  eliinid  43409  suprnmpt  43479  wessf1ornlem  43491  fompt  43499  disjinfi  43500  choicefi  43508  axccdom  43530  axccd  43537  rnmptlb  43557  rnmptbddlem  43558  rnmptbd2lem  43563  upbdrech  43626  ssfiunibd  43630  iuneqfzuzlem  43655  xrralrecnnle  43704  supxrunb3  43720  supxrleubrnmpt  43727  unb2ltle  43736  rexabslelem  43739  suprleubrnmpt  43743  uzublem  43751  infxrgelbrnmpt  43775  cvgcaule  43813  fprodcnlem  43926  limcrecl  43956  islpcn  43966  limsupre  43968  limcleqr  43971  0ellimcdiv  43976  limclner  43978  climinf2lem  44033  climinf3  44043  limsupmnflem  44047  limsupmnfuzlem  44053  limsupre3uzlem  44062  climisp  44073  climrescn  44075  climxrrelem  44076  climxrre  44077  climxlim2lem  44172  cncfshift  44201  cncfperiod  44206  cncfuni  44213  cncfioobd  44224  dvbdfbdioolem1  44255  dvnprodlem2  44274  stoweidlem28  44355  stoweidlem29  44356  stoweidlem31  44358  stoweidlem60  44387  stoweidlem62  44389  fourierdlem39  44473  fourierdlem68  44501  fourierdlem73  44506  fourierdlem77  44510  fourierdlem80  44513  fourierdlem83  44516  fourierdlem87  44520  fourierdlem94  44527  fourierdlem103  44536  fourierdlem104  44537  fourierdlem112  44545  fourierdlem113  44546  qndenserrnbllem  44621  dfsalgen2  44668  subsaliuncl  44685  sge0lefi  44725  sge0isum  44754  sge0reuzb  44775  iundjiun  44787  voliunsge0lem  44799  meaiuninclem  44807  meaiuninc3v  44811  isomenndlem  44857  ovnsubaddlem2  44898  hoidmvlelem3  44924  hoidmvlelem5  44926  hspdifhsp  44943  hoiqssbllem3  44951  hspmbllem2  44954  vonioo  45009  vonicc  45012  pimdecfgtioo  45044  issmflem  45054  issmfle  45072  issmfgt  45083  issmfgelem  45096  smflimlem2  45099  smfinflem  45144  smflimsuplem5  45151  smfliminflem  45157  fsupdm  45169  finfdm  45173  sbgoldbm  46062  sbgoldbo  46065  aacllem  47334
  Copyright terms: Public domain W3C validator