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

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

Proof of Theorem rsp
StepHypRef Expression
1 df-ral 3114 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 sp 2181 . 2 (∀𝑥(𝑥𝐴𝜑) → (𝑥𝐴𝜑))
31, 2sylbi 220 1 (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1536  wcel 2112  wral 3109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2176
This theorem depends on definitions:  df-bi 210  df-ex 1782  df-ral 3114
This theorem is referenced by:  rspa  3174  rspec  3175  rsp2  3180  r19.12  3286  2reu1  3829  reupick2  4244  rspn0OLD  4270  iuneqconst  4895  dfiun2gOLD  4921  iinss2  4947  invdisj  5017  reusv1  5266  reusv2lem1  5267  reusv2lem3  5269  reusv3  5274  ralxfrALT  5284  fvmptss  6761  ffnfv  6863  riota5f  7125  mpoeq123  7209  peano5  7589  wfrlem4  7945  wfrlem12  7953  tfr3  8022  tz7.48-1  8066  tz7.49  8068  nneneq  8688  scottex  9302  dfac2b  9545  infpssrlem4  9721  fin23lem30  9757  fin23lem31  9758  hsmexlem2  9842  domtriomlem  9857  axdc3lem2  9866  axdc3lem4  9868  konigthlem  9983  winalim2  10111  nqereu  10344  dedekind  10796  dedekindle  10797  prodeq2ii  15262  vdwlem9  16318  mreiincl  16862  sgrpidmnd  17911  srgi  19257  ringi  19309  lbsextlem3  19928  lbsextlem4  19929  tgcl  21577  txindis  22242  alexsubALTlem3  22657  prdsxmslem2  23139  fsumcn  23478  lebnumlem1  23569  iscmet3lem1  23898  iscmet3lem2  23899  ovoliunlem2  24110  mbfimaopnlem  24262  limciun  24500  ftalem3  25663  ostth3  26225  mptelee  26692  ubthlem2  28657  aciunf1lem  30428  esumcvg  31453  bnj228  32113  bnj590  32290  bnj594  32292  bnj600  32299  bnj1128  32370  bnj1125  32372  bnj1145  32373  bnj1398  32414  bnj1417  32421  dfon2lem3  33138  dfon2lem7  33142  trpredmintr  33178  frr3g  33229  frrlem4  33234  frrlem8  33238  frrlem10  33240  frrlem13  33243  sslttr  33376  neibastop1  33815  unblimceq0lem  33953  unbdqndv2  33958  rdgssun  34790  ralssiun  34819  fvineqsneu  34823  fvineqsneq  34824  cover2  35145  upixp  35160  indexdom  35165  filbcmb  35171  mettrifi  35188  mpobi123f  35593  riotasvd  36245  glbconxN  36667  cdlemefr29exN  37691  cdlemk36  38202  mptfcl  39648  aomclem2  39986  hbtlem5  40059  gneispace  40824  trintALTVD  41573  trintALT  41574  refsumcn  41646  rfcnnnub  41652  choicefi  41816  mullimc  42245  mullimcf  42252  addlimc  42277  itgsubsticclem  42604  stoweidlem25  42654  stoweidlem52  42681  stoweidlem59  42688  stoweidlem62  42691  wallispilem3  42696  stirlinglem13  42715  fourierdlem73  42808  ffnafv  43714  iunord  45193  setrec1lem2  45205
  Copyright terms: Public domain W3C validator