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

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

Proof of Theorem rspa
StepHypRef Expression
1 rsp 2913 . 2 (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))
21imp 444 1 ((∀𝑥𝐴 𝜑𝑥𝐴) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 1977  wral 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901
This theorem is referenced by:  ralbi  3050  mpteq12f  4661  reusv2lem2  4795  reusv2lem2OLD  4796  axdc4lem  9160  fprodle  14566  isucn2  21893  bcthlem5  22933  gausslemma2dlem6  24897  foresf1o  28727  abrexss  28734  reff  29234  locfinreflem  29235  cmpcref  29245  ldgenpisyslem1  29553  voliune  29619  volfiniune  29620  bnj1366  30154  heicant  32614  indexdom  32699  glbconxN  33682  pmapglbx  34073  pmapglb2xN  34076  mzpexpmpt  36326  uzwo4  38246  ralimralim  38279  eliinid  38325  suprnmpt  38350  wessf1ornlem  38366  fompt  38374  disjinfi  38375  fvixp2  38384  choicefi  38387  axccdom  38411  axccd  38424  upbdrech  38460  ssfiunibd  38464  iuneqfzuzlem  38491  xrralrecnnle  38543  fprodcnlem  38666  limcrecl  38696  islpcn  38706  limsupre  38708  limcleqr  38711  0ellimcdiv  38716  limclner  38718  cncfshift  38759  cncfperiod  38764  cncfuni  38772  cncfioobd  38783  dvbdfbdioolem1  38818  dvnprodlem2  38837  stoweidlem28  38921  stoweidlem29  38922  stoweidlem31  38924  stoweidlem60  38953  stoweidlem62  38955  fourierdlem39  39039  fourierdlem68  39067  fourierdlem73  39072  fourierdlem77  39076  fourierdlem80  39079  fourierdlem83  39082  fourierdlem87  39086  fourierdlem94  39093  fourierdlem103  39102  fourierdlem104  39103  fourierdlem112  39111  fourierdlem113  39112  qndenserrnbllem  39190  dfsalgen2  39235  subsaliuncl  39252  sge0lefi  39291  sge0isum  39320  sge0reuzb  39341  iundjiun  39353  voliunsge0lem  39365  meaiuninclem  39373  isomenndlem  39420  ovnsubaddlem2  39461  hoidmvlelem3  39487  hoidmvlelem5  39489  hspdifhsp  39506  hoiqssbllem3  39514  hspmbllem2  39517  vonioo  39573  vonicc  39576  pimdecfgtioo  39604  issmflem  39613  issmfle  39632  issmfgt  39643  issmfgelem  39655  smflimlem2  39658  aacllem  42356
  Copyright terms: Public domain W3C validator