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

Theorem rsp 2603
Description: Restricted specialization. (Contributed by NM, 17-Oct-1996.)
Assertion
Ref Expression
rsp  |-  ( A. x  e.  A  ph  ->  ( x  e.  A  ->  ph ) )

Proof of Theorem rsp
StepHypRef Expression
1 df-ral 2548 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 sp 1716 . 2  |-  ( A. x ( x  e.  A  ->  ph )  -> 
( x  e.  A  ->  ph ) )
31, 2sylbi 187 1  |-  ( A. x  e.  A  ph  ->  ( x  e.  A  ->  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527    e. wcel 1684   A.wral 2543
This theorem is referenced by:  rsp2  2605  rspec  2607  r19.12  2656  ralbi  2679  reupick2  3454  dfiun2g  3935  iinss2  3954  invdisj  4012  mpteq12f  4096  trss  4122  reusv1  4534  reusv2lem1  4535  reusv2lem2  4536  reusv2lem3  4537  reusv3  4542  ralxfrALT  4553  peano5  4679  fun11iun  5493  fvmptss  5609  ffnfv  5685  mpt2eq123  5907  riota5f  6329  riotasvd  6347  riotasvdOLD  6348  tfr3  6415  tz7.48-1  6455  tz7.49  6457  nneneq  7044  scottex  7555  dfac2  7757  infpssrlem4  7932  fin23lem30  7968  fin23lem31  7969  hsmexlem2  8053  domtriomlem  8068  axdc3lem2  8077  axdc3lem4  8079  axdc4lem  8081  konigthlem  8190  winalim2  8318  nqereu  8553  sumeq2ii  12166  vdwlem9  13036  mreiincl  13498  rngi  15353  lbsextlem3  15913  lbsextlem4  15914  tgcl  16707  txindis  17328  alexsubALTlem3  17743  prdsxmslem2  18075  fsumcn  18374  lebnumlem1  18459  iscmet3lem1  18717  iscmet3lem2  18718  bcthlem5  18750  ovoliunlem2  18862  mbfimaopnlem  19010  limciun  19244  ftalem3  20312  ostth3  20787  ubthlem2  21450  esumcvg  23454  dedekind  24082  dedekindle  24083  dfon2lem3  24141  dfon2lem7  24145  trpredmintr  24234  wfrlem4  24259  wfrlem12  24267  frr3g  24280  frrlem4  24284  frrlem11  24293  mptelee  24523  imgfldref2  25064  intopcoaconc  25541  prcnt  25551  cmptdst  25568  cmpmon  25815  neibastop1  26308  cover2  26358  upixp  26403  indexdom  26413  filbcmb  26432  mettrifi  26473  mptfcl  26798  mzpexpmpt  26823  aomclem2  27152  hbtlem5  27332  refsumcn  27701  rfcnnnub  27707  stoweidlem5  27754  stoweidlem25  27774  stoweidlem28  27777  stoweidlem29  27778  stoweidlem31  27780  stoweidlem44  27793  stoweidlem45  27794  stoweidlem48  27797  stoweidlem52  27801  stoweidlem54  27803  stoweidlem59  27808  stoweidlem60  27809  stoweidlem62  27811  wallispilem3  27816  stirlinglem13  27835  2reu1  27964  ffnafv  28033  trintALTVD  28656  trintALT  28657  bnj228  28763  bnj1366  28862  bnj590  28942  bnj594  28944  bnj600  28951  bnj1128  29020  bnj1125  29022  bnj1145  29023  bnj1398  29064  bnj1417  29071  glbconxN  29567  pmapglbx  29958  pmapglb2xN  29961  cdlemefr29exN  30591  cdlemk36  31102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-ral 2548
  Copyright terms: Public domain W3C validator