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

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

Proof of Theorem rspa
StepHypRef Expression
1 rsp 3205 . 2 (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))
21imp 407 1 ((∀𝑥𝐴 𝜑𝑥𝐴) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2105  wral 3138
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-12 2167
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-ral 3143
This theorem is referenced by:  r19.21bi  3208  ralbiOLD  3233  ralrexbidOLD  3323  dfiun2g  4947  mpteq12f  5141  reusv2lem2  5291  axdc4lem  9866  fprodle  15340  isucn2  22817  bcthlem5  23860  gausslemma2dlem6  25876  opreu2reuALT  30168  foresf1o  30193  abrexss  30200  reff  31003  locfinreflem  31004  cmpcref  31014  ldgenpisyslem1  31322  voliune  31388  volfiniune  31389  reprpmtf1o  31797  bnj1366  32001  frrlem12  33032  heicant  34809  indexdom  34892  glbconxN  36396  pmapglbx  36787  pmapglb2xN  36790  mzpexpmpt  39222  uzwo4  41195  ralimralim  41225  eliinid  41258  ralimda  41286  suprnmpt  41310  wessf1ornlem  41325  fompt  41333  disjinfi  41334  choicefi  41343  axccdom  41367  axccd  41375  rnmptlb  41394  rnmptbddlem  41395  rnmptbd2lem  41400  upbdrech  41452  ssfiunibd  41456  iuneqfzuzlem  41482  xrralrecnnle  41533  supxrunb3  41552  supxrleubrnmpt  41559  unb2ltle  41569  rexabslelem  41572  suprleubrnmpt  41576  uzublem  41584  infxrgelbrnmpt  41610  fprodcnlem  41760  limcrecl  41790  islpcn  41800  limsupre  41802  limcleqr  41805  0ellimcdiv  41810  limclner  41812  climinf2lem  41867  climinf3  41877  limsupmnflem  41881  limsupmnfuzlem  41887  limsupre3uzlem  41896  climisp  41907  climrescn  41909  climxrrelem  41910  climxrre  41911  climxlim2lem  42006  cncfshift  42037  cncfperiod  42042  cncfuni  42049  cncfioobd  42060  dvbdfbdioolem1  42093  dvnprodlem2  42112  stoweidlem28  42194  stoweidlem29  42195  stoweidlem31  42197  stoweidlem60  42226  stoweidlem62  42228  fourierdlem39  42312  fourierdlem68  42340  fourierdlem73  42345  fourierdlem77  42349  fourierdlem80  42352  fourierdlem83  42355  fourierdlem87  42359  fourierdlem94  42366  fourierdlem103  42375  fourierdlem104  42376  fourierdlem112  42384  fourierdlem113  42385  qndenserrnbllem  42460  dfsalgen2  42505  subsaliuncl  42522  sge0lefi  42561  sge0isum  42590  sge0reuzb  42611  iundjiun  42623  voliunsge0lem  42635  meaiuninclem  42643  meaiuninc3v  42647  isomenndlem  42693  ovnsubaddlem2  42734  hoidmvlelem3  42760  hoidmvlelem5  42762  hspdifhsp  42779  hoiqssbllem3  42787  hspmbllem2  42790  vonioo  42845  vonicc  42848  pimdecfgtioo  42876  issmflem  42885  issmfle  42903  issmfgt  42914  issmfgelem  42926  smflimlem2  42929  smfinflem  42972  smflimsuplem5  42979  smfliminflem  42985  sbgoldbm  43796  sbgoldbo  43799  aacllem  44800
  Copyright terms: Public domain W3C validator