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

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

Proof of Theorem rsp
StepHypRef Expression
1 df-ral 2900 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 sp 2040 . 2 (∀𝑥(𝑥𝐴𝜑) → (𝑥𝐴𝜑))
31, 2sylbi 205 1 (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1472  wcel 1976  wral 2895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-12 2033
This theorem depends on definitions:  df-bi 195  df-ex 1695  df-ral 2900
This theorem is referenced by:  rspa  2913  rspec  2914  r19.21bi  2915  rsp2  2919  r19.12  3044  reupick2  3871  rspn0  3891  dfiun2g  4482  iinss2  4502  invdisj  4565  trssOLD  4684  reusv1  4787  reusv1OLD  4788  reusv2lem1  4789  reusv2lem3  4792  reusv3  4797  ralxfrALT  4808  fvmptss  6186  ffnfv  6280  riota5f  6513  mpt2eq123  6590  peano5  6959  fun11iun  6997  wfrlem4  7283  wfrlem12  7291  tfr3  7360  tz7.48-1  7403  tz7.49  7405  nneneq  8006  scottex  8609  dfac2  8814  infpssrlem4  8989  fin23lem30  9025  fin23lem31  9026  hsmexlem2  9110  domtriomlem  9125  axdc3lem2  9134  axdc3lem4  9136  konigthlem  9247  winalim2  9375  nqereu  9608  dedekind  10052  dedekindle  10053  prodeq2ii  14431  vdwlem9  15480  mreiincl  16028  srgi  18283  ringi  18332  lbsextlem3  18930  lbsextlem4  18931  tgcl  20532  txindis  21195  alexsubALTlem3  21611  prdsxmslem2  22092  fsumcn  22429  lebnumlem1  22516  iscmet3lem1  22842  iscmet3lem2  22843  ovoliunlem2  23023  mbfimaopnlem  23173  limciun  23409  ftalem3  24546  ostth3  25072  mptelee  25521  ubthlem2  26945  aciunf1lem  28678  esumcvg  29309  bnj228  29891  bnj590  30068  bnj594  30070  bnj600  30077  bnj1128  30146  bnj1125  30148  bnj1145  30149  bnj1398  30190  bnj1417  30197  dfon2lem3  30768  dfon2lem7  30772  trpredmintr  30809  frr3g  30857  frrlem4  30861  frrlem11  30870  neibastop1  31358  unblimceq0lem  31501  unbdqndv2  31506  cover2  32502  upixp  32518  indexdom  32523  filbcmb  32529  mettrifi  32547  mpt2bi123f  32965  riotasvd  33084  glbconxN  33506  cdlemefr29exN  34532  cdlemk36  35043  mptfcl  36125  aomclem2  36467  hbtlem5  36541  gneispace  37276  trintALTVD  37962  trintALT  37963  refsumcn  38036  rfcnnnub  38042  choicefi  38211  mullimc  38507  mullimcf  38514  addlimc  38539  itgsubsticclem  38691  stoweidlem25  38742  stoweidlem52  38769  stoweidlem59  38776  stoweidlem62  38779  wallispilem3  38784  stirlinglem13  38803  fourierdlem73  38896  2reu1  39659  ffnafv  39725
  Copyright terms: Public domain W3C validator