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

Theorem rsp 3055
Description: Restricted specialization. (Contributed by NM, 17-Oct-1996.)
Assertion
Ref Expression
rsp (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))

Proof of Theorem rsp
StepHypRef Expression
1 df-ral 3043 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 sp 2188 . 2 (∀𝑥(𝑥𝐴𝜑) → (𝑥𝐴𝜑))
31, 2sylbi 207 1 (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1618  wcel 2127  wral 3038
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-12 2184
This theorem depends on definitions:  df-bi 197  df-ex 1842  df-ral 3043
This theorem is referenced by:  rspa  3056  rspec  3057  r19.21bi  3058  rsp2  3062  r19.12  3189  reupick2  4044  rspn0  4065  dfiun2g  4692  iinss2  4712  invdisj  4778  trssOLD  4902  reusv1  5003  reusv1OLD  5004  reusv2lem1  5005  reusv2lem3  5008  reusv3  5013  ralxfrALT  5024  fvmptss  6442  ffnfv  6539  riota5f  6787  mpt2eq123  6867  peano5  7242  fun11iun  7279  wfrlem4  7575  wfrlem12  7583  tfr3  7652  tz7.48-1  7695  tz7.49  7697  nneneq  8296  scottex  8909  dfac2b  9114  dfac2OLD  9116  infpssrlem4  9291  fin23lem30  9327  fin23lem31  9328  hsmexlem2  9412  domtriomlem  9427  axdc3lem2  9436  axdc3lem4  9438  konigthlem  9553  winalim2  9681  nqereu  9914  dedekind  10363  dedekindle  10364  prodeq2ii  14813  vdwlem9  15866  mreiincl  16429  srgi  18682  ringi  18731  lbsextlem3  19333  lbsextlem4  19334  tgcl  20946  txindis  21610  alexsubALTlem3  22025  prdsxmslem2  22506  fsumcn  22845  lebnumlem1  22932  iscmet3lem1  23260  iscmet3lem2  23261  ovoliunlem2  23442  mbfimaopnlem  23592  limciun  23828  ftalem3  24971  ostth3  25497  mptelee  25945  ubthlem2  28007  aciunf1lem  29742  esumcvg  30428  bnj228  31081  bnj590  31258  bnj594  31260  bnj600  31267  bnj1128  31336  bnj1125  31338  bnj1145  31339  bnj1398  31380  bnj1417  31387  dfon2lem3  31966  dfon2lem7  31970  trpredmintr  32007  frr3g  32056  frrlem4  32060  frrlem11  32069  sslttr  32191  neibastop1  32631  unblimceq0lem  32774  unbdqndv2  32779  cover2  33790  upixp  33806  indexdom  33811  filbcmb  33817  mettrifi  33835  mpt2bi123f  34253  riotasvd  34714  glbconxN  35136  cdlemefr29exN  36161  cdlemk36  36672  mptfcl  37754  aomclem2  38096  hbtlem5  38169  gneispace  38903  trintALTVD  39584  trintALT  39585  refsumcn  39657  rfcnnnub  39663  choicefi  39860  mullimc  40320  mullimcf  40327  addlimc  40352  itgsubsticclem  40663  stoweidlem25  40714  stoweidlem52  40741  stoweidlem59  40748  stoweidlem62  40751  wallispilem3  40756  stirlinglem13  40775  fourierdlem73  40868  2reu1  41661  ffnafv  41726  iunord  42901  setrec1lem2  42914
  Copyright terms: Public domain W3C validator