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

Theorem rsp 2616
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 2561 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 sp 1728 . 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 1530    e. wcel 1696   A.wral 2556
This theorem is referenced by:  rsp2  2618  rspec  2620  r19.12  2669  ralbi  2692  reupick2  3467  dfiun2g  3951  iinss2  3970  invdisj  4028  mpteq12f  4112  trss  4138  reusv1  4550  reusv2lem1  4551  reusv2lem2  4552  reusv2lem3  4553  reusv3  4558  ralxfrALT  4569  peano5  4695  fun11iun  5509  fvmptss  5625  ffnfv  5701  mpt2eq123  5923  riota5f  6345  riotasvd  6363  riotasvdOLD  6364  tfr3  6431  tz7.48-1  6471  tz7.49  6473  nneneq  7060  scottex  7571  dfac2  7773  infpssrlem4  7948  fin23lem30  7984  fin23lem31  7985  hsmexlem2  8069  domtriomlem  8084  axdc3lem2  8093  axdc3lem4  8095  axdc4lem  8097  konigthlem  8206  winalim2  8334  nqereu  8569  sumeq2ii  12182  vdwlem9  13052  mreiincl  13514  rngi  15369  lbsextlem3  15929  lbsextlem4  15930  tgcl  16723  txindis  17344  alexsubALTlem3  17759  prdsxmslem2  18091  fsumcn  18390  lebnumlem1  18475  iscmet3lem1  18733  iscmet3lem2  18734  bcthlem5  18766  ovoliunlem2  18878  mbfimaopnlem  19026  limciun  19260  ftalem3  20328  ostth3  20803  ubthlem2  21466  esumcvg  23469  dedekind  24097  dedekindle  24098  cprodeq2ii  24135  dfon2lem3  24212  dfon2lem7  24216  trpredmintr  24305  wfrlem4  24330  wfrlem12  24338  frr3g  24351  frrlem4  24355  frrlem11  24364  mptelee  24595  imgfldref2  25167  intopcoaconc  25644  prcnt  25654  cmptdst  25671  cmpmon  25918  neibastop1  26411  cover2  26461  upixp  26506  indexdom  26516  filbcmb  26535  mettrifi  26576  mptfcl  26901  mzpexpmpt  26926  aomclem2  27255  hbtlem5  27435  refsumcn  27804  rfcnnnub  27810  stoweidlem5  27857  stoweidlem25  27877  stoweidlem28  27880  stoweidlem29  27881  stoweidlem31  27883  stoweidlem44  27896  stoweidlem45  27897  stoweidlem48  27900  stoweidlem52  27904  stoweidlem54  27906  stoweidlem59  27911  stoweidlem60  27912  stoweidlem62  27914  wallispilem3  27919  stirlinglem13  27938  2reu1  28067  ffnafv  28139  trintALTVD  28972  trintALT  28973  bnj228  29079  bnj1366  29178  bnj590  29258  bnj594  29260  bnj600  29267  bnj1128  29336  bnj1125  29338  bnj1145  29339  bnj1398  29380  bnj1417  29387  glbconxN  30189  pmapglbx  30580  pmapglb2xN  30583  cdlemefr29exN  31213  cdlemk36  31724
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-ral 2561
  Copyright terms: Public domain W3C validator