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

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

Proof of Theorem rsp
StepHypRef Expression
1 df-ral 2946 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 sp 2091 . 2 (∀𝑥(𝑥𝐴𝜑) → (𝑥𝐴𝜑))
31, 2sylbi 207 1 (∀𝑥𝐴 𝜑 → (𝑥𝐴𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1521  wcel 2030  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087
This theorem depends on definitions:  df-bi 197  df-ex 1745  df-ral 2946
This theorem is referenced by:  rspa  2959  rspec  2960  r19.21bi  2961  rsp2  2965  r19.12  3092  reupick2  3946  rspn0  3967  dfiun2g  4584  iinss2  4604  invdisj  4670  trssOLD  4795  reusv1  4896  reusv1OLD  4897  reusv2lem1  4898  reusv2lem3  4901  reusv3  4906  ralxfrALT  4917  fvmptss  6331  ffnfv  6428  riota5f  6676  mpt2eq123  6756  peano5  7131  fun11iun  7168  wfrlem4  7463  wfrlem12  7471  tfr3  7540  tz7.48-1  7583  tz7.49  7585  nneneq  8184  scottex  8786  dfac2  8991  infpssrlem4  9166  fin23lem30  9202  fin23lem31  9203  hsmexlem2  9287  domtriomlem  9302  axdc3lem2  9311  axdc3lem4  9313  konigthlem  9428  winalim2  9556  nqereu  9789  dedekind  10238  dedekindle  10239  prodeq2ii  14687  vdwlem9  15740  mreiincl  16303  srgi  18557  ringi  18606  lbsextlem3  19208  lbsextlem4  19209  tgcl  20821  txindis  21485  alexsubALTlem3  21900  prdsxmslem2  22381  fsumcn  22720  lebnumlem1  22807  iscmet3lem1  23135  iscmet3lem2  23136  ovoliunlem2  23317  mbfimaopnlem  23467  limciun  23703  ftalem3  24846  ostth3  25372  mptelee  25820  ubthlem2  27855  aciunf1lem  29590  esumcvg  30276  bnj228  30929  bnj590  31106  bnj594  31108  bnj600  31115  bnj1128  31184  bnj1125  31186  bnj1145  31187  bnj1398  31228  bnj1417  31235  dfon2lem3  31814  dfon2lem7  31818  trpredmintr  31855  frr3g  31904  frrlem4  31908  frrlem11  31917  sslttr  32039  neibastop1  32479  unblimceq0lem  32622  unbdqndv2  32627  cover2  33638  upixp  33654  indexdom  33659  filbcmb  33665  mettrifi  33683  mpt2bi123f  34101  riotasvd  34560  glbconxN  34982  cdlemefr29exN  36007  cdlemk36  36518  mptfcl  37600  aomclem2  37942  hbtlem5  38015  gneispace  38749  trintALTVD  39430  trintALT  39431  refsumcn  39503  rfcnnnub  39509  choicefi  39706  mullimc  40166  mullimcf  40173  addlimc  40198  itgsubsticclem  40509  stoweidlem25  40560  stoweidlem52  40587  stoweidlem59  40594  stoweidlem62  40597  wallispilem3  40602  stirlinglem13  40621  fourierdlem73  40714  2reu1  41507  ffnafv  41572  iunord  42747  setrec1lem2  42760
  Copyright terms: Public domain W3C validator