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

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

Proof of Theorem rspa
StepHypRef Expression
1 rsp 3202 . 2 (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))
21imp 407 1 ((∀𝑥𝐴 𝜑𝑥𝐴) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2105  wral 3135
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 3140
This theorem is referenced by:  r19.21bi  3205  ralbiOLD  3230  ralrexbidOLD  3320  dfiun2g  4946  mpteq12f  5140  reusv2lem2  5290  axdc4lem  9865  fprodle  15338  isucn2  22815  bcthlem5  23858  gausslemma2dlem6  25875  opreu2reuALT  30167  foresf1o  30192  abrexss  30199  reff  31002  locfinreflem  31003  cmpcref  31013  ldgenpisyslem1  31321  voliune  31387  volfiniune  31388  reprpmtf1o  31796  bnj1366  32000  frrlem12  33031  heicant  34808  indexdom  34890  glbconxN  36394  pmapglbx  36785  pmapglb2xN  36788  mzpexpmpt  39220  uzwo4  41192  ralimralim  41222  eliinid  41254  ralimda  41282  suprnmpt  41306  wessf1ornlem  41321  fompt  41329  disjinfi  41330  choicefi  41339  axccdom  41363  axccd  41371  rnmptlb  41390  rnmptbddlem  41391  rnmptbd2lem  41396  upbdrech  41448  ssfiunibd  41452  iuneqfzuzlem  41478  xrralrecnnle  41529  supxrunb3  41548  supxrleubrnmpt  41555  unb2ltle  41565  rexabslelem  41568  suprleubrnmpt  41572  uzublem  41580  infxrgelbrnmpt  41606  fprodcnlem  41756  limcrecl  41786  islpcn  41796  limsupre  41798  limcleqr  41801  0ellimcdiv  41806  limclner  41808  climinf2lem  41863  climinf3  41873  limsupmnflem  41877  limsupmnfuzlem  41883  limsupre3uzlem  41892  climisp  41903  climrescn  41905  climxrrelem  41906  climxrre  41907  climxlim2lem  42002  cncfshift  42033  cncfperiod  42038  cncfuni  42045  cncfioobd  42056  dvbdfbdioolem1  42089  dvnprodlem2  42108  stoweidlem28  42190  stoweidlem29  42191  stoweidlem31  42193  stoweidlem60  42222  stoweidlem62  42224  fourierdlem39  42308  fourierdlem68  42336  fourierdlem73  42341  fourierdlem77  42345  fourierdlem80  42348  fourierdlem83  42351  fourierdlem87  42355  fourierdlem94  42362  fourierdlem103  42371  fourierdlem104  42372  fourierdlem112  42380  fourierdlem113  42381  qndenserrnbllem  42456  dfsalgen2  42501  subsaliuncl  42518  sge0lefi  42557  sge0isum  42586  sge0reuzb  42607  iundjiun  42619  voliunsge0lem  42631  meaiuninclem  42639  meaiuninc3v  42643  isomenndlem  42689  ovnsubaddlem2  42730  hoidmvlelem3  42756  hoidmvlelem5  42758  hspdifhsp  42775  hoiqssbllem3  42783  hspmbllem2  42786  vonioo  42841  vonicc  42844  pimdecfgtioo  42872  issmflem  42881  issmfle  42899  issmfgt  42910  issmfgelem  42922  smflimlem2  42925  smfinflem  42968  smflimsuplem5  42975  smfliminflem  42981  sbgoldbm  43826  sbgoldbo  43829  aacllem  44830
  Copyright terms: Public domain W3C validator