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

Theorem rsp 2702
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 2647 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 sp 1755 . 2  |-  ( A. x ( x  e.  A  ->  ph )  -> 
( x  e.  A  ->  ph ) )
31, 2sylbi 188 1  |-  ( A. x  e.  A  ph  ->  ( x  e.  A  ->  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1546    e. wcel 1717   A.wral 2642
This theorem is referenced by:  rsp2  2704  rspec  2706  r19.12  2755  ralbi  2778  reupick2  3563  dfiun2g  4058  iinss2  4077  invdisj  4135  mpteq12f  4219  trss  4245  reusv1  4656  reusv2lem1  4657  reusv2lem2  4658  reusv2lem3  4659  reusv3  4664  ralxfrALT  4675  peano5  4801  fun11iun  5628  fvmptss  5745  ffnfv  5826  mpt2eq123  6065  riota5f  6503  riotasvd  6521  riotasvdOLD  6522  tfr3  6589  tz7.48-1  6629  tz7.49  6631  nneneq  7219  scottex  7735  dfac2  7937  infpssrlem4  8112  fin23lem30  8148  fin23lem31  8149  hsmexlem2  8233  domtriomlem  8248  axdc3lem2  8257  axdc3lem4  8259  axdc4lem  8261  konigthlem  8369  winalim2  8497  nqereu  8732  sumeq2ii  12407  vdwlem9  13277  mreiincl  13741  rngi  15596  lbsextlem3  16152  lbsextlem4  16153  tgcl  16950  txindis  17580  alexsubALTlem3  17994  isucn2  18223  prdsxmslem2  18442  fsumcn  18764  lebnumlem1  18850  iscmet3lem1  19108  iscmet3lem2  19109  bcthlem5  19143  ovoliunlem2  19259  mbfimaopnlem  19407  limciun  19641  ftalem3  20717  ostth3  21192  ubthlem2  22214  esumcvg  24265  dedekind  24959  dedekindle  24960  prodeq2ii  25011  dfon2lem3  25158  dfon2lem7  25162  trpredmintr  25251  wfrlem4  25276  wfrlem12  25284  frr3g  25297  frrlem4  25301  frrlem11  25310  mptelee  25541  neibastop1  26072  cover2  26099  upixp  26115  indexdom  26120  filbcmb  26126  mettrifi  26147  mptfcl  26461  mzpexpmpt  26486  aomclem2  26814  hbtlem5  26994  refsumcn  27362  rfcnnnub  27368  stoweidlem25  27435  stoweidlem28  27438  stoweidlem29  27439  stoweidlem31  27441  stoweidlem52  27462  stoweidlem59  27469  stoweidlem60  27470  stoweidlem62  27472  wallispilem3  27477  stirlinglem13  27496  2reu1  27625  ffnafv  27697  trintALTVD  28326  trintALT  28327  bnj228  28433  bnj1366  28532  bnj590  28612  bnj594  28614  bnj600  28621  bnj1128  28690  bnj1125  28692  bnj1145  28693  bnj1398  28734  bnj1417  28741  glbconxN  29543  pmapglbx  29934  pmapglb2xN  29937  cdlemefr29exN  30567  cdlemk36  31078
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-ral 2647
  Copyright terms: Public domain W3C validator