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

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

Proof of Theorem rsp
StepHypRef Expression
1 df-ral 2913 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 sp 2051 . 2 (∀𝑥(𝑥𝐴𝜑) → (𝑥𝐴𝜑))
31, 2sylbi 207 1 (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1478  wcel 1987  wral 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-12 2044
This theorem depends on definitions:  df-bi 197  df-ex 1702  df-ral 2913
This theorem is referenced by:  rspa  2926  rspec  2927  r19.21bi  2928  rsp2  2932  r19.12  3058  reupick2  3895  rspn0  3916  dfiun2g  4525  iinss2  4545  invdisj  4611  trssOLD  4732  reusv1  4836  reusv1OLD  4837  reusv2lem1  4838  reusv2lem3  4841  reusv3  4846  ralxfrALT  4857  fvmptss  6259  ffnfv  6354  riota5f  6601  mpt2eq123  6679  peano5  7051  fun11iun  7088  wfrlem4  7378  wfrlem12  7386  tfr3  7455  tz7.48-1  7498  tz7.49  7500  nneneq  8103  scottex  8708  dfac2  8913  infpssrlem4  9088  fin23lem30  9124  fin23lem31  9125  hsmexlem2  9209  domtriomlem  9224  axdc3lem2  9233  axdc3lem4  9235  konigthlem  9350  winalim2  9478  nqereu  9711  dedekind  10160  dedekindle  10161  prodeq2ii  14587  vdwlem9  15636  mreiincl  16196  srgi  18451  ringi  18500  lbsextlem3  19100  lbsextlem4  19101  tgcl  20713  txindis  21377  alexsubALTlem3  21793  prdsxmslem2  22274  fsumcn  22613  lebnumlem1  22700  iscmet3lem1  23029  iscmet3lem2  23030  ovoliunlem2  23211  mbfimaopnlem  23362  limciun  23598  ftalem3  24735  ostth3  25261  mptelee  25709  ubthlem2  27615  aciunf1lem  29345  esumcvg  29971  bnj228  30564  bnj590  30741  bnj594  30743  bnj600  30750  bnj1128  30819  bnj1125  30821  bnj1145  30822  bnj1398  30863  bnj1417  30870  dfon2lem3  31444  dfon2lem7  31448  trpredmintr  31485  frr3g  31533  frrlem4  31537  frrlem11  31546  neibastop1  32049  unblimceq0lem  32192  unbdqndv2  32197  cover2  33179  upixp  33195  indexdom  33200  filbcmb  33206  mettrifi  33224  mpt2bi123f  33642  riotasvd  33761  glbconxN  34183  cdlemefr29exN  35209  cdlemk36  35720  mptfcl  36802  aomclem2  37144  hbtlem5  37218  gneispace  37953  trintALTVD  38638  trintALT  38639  refsumcn  38711  rfcnnnub  38717  choicefi  38901  mullimc  39284  mullimcf  39291  addlimc  39316  itgsubsticclem  39528  stoweidlem25  39579  stoweidlem52  39606  stoweidlem59  39613  stoweidlem62  39616  wallispilem3  39621  stirlinglem13  39640  fourierdlem73  39733  2reu1  40520  ffnafv  40585  iunord  41744  setrec1lem2  41758
  Copyright terms: Public domain W3C validator