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

Theorem rsp 2758
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 2702 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 sp 1763 . 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 1549    e. wcel 1725   A.wral 2697
This theorem is referenced by:  rsp2  2760  rspec  2762  r19.12  2811  ralbi  2834  reupick2  3619  dfiun2g  4115  iinss2  4135  invdisj  4193  mpteq12f  4277  trss  4303  reusv1  4715  reusv2lem1  4716  reusv2lem2  4717  reusv2lem3  4718  reusv3  4723  ralxfrALT  4734  peano5  4860  fun11iun  5687  fvmptss  5805  ffnfv  5886  mpt2eq123  6125  riota5f  6566  riotasvd  6584  riotasvdOLD  6585  tfr3  6652  tz7.48-1  6692  tz7.49  6694  nneneq  7282  scottex  7801  dfac2  8003  infpssrlem4  8178  fin23lem30  8214  fin23lem31  8215  hsmexlem2  8299  domtriomlem  8314  axdc3lem2  8323  axdc3lem4  8325  axdc4lem  8327  konigthlem  8435  winalim2  8563  nqereu  8798  sumeq2ii  12479  vdwlem9  13349  mreiincl  13813  rngi  15668  lbsextlem3  16224  lbsextlem4  16225  tgcl  17026  txindis  17658  alexsubALTlem3  18072  isucn2  18301  prdsxmslem2  18551  fsumcn  18892  lebnumlem1  18978  iscmet3lem1  19236  iscmet3lem2  19237  bcthlem5  19273  ovoliunlem2  19391  mbfimaopnlem  19539  limciun  19773  ftalem3  20849  ostth3  21324  ubthlem2  22365  esumcvg  24468  dedekind  25179  dedekindle  25180  prodeq2ii  25231  dfon2lem3  25404  dfon2lem7  25408  trpredmintr  25501  wfrlem4  25533  wfrlem12  25541  frr3g  25573  frrlem4  25577  frrlem11  25586  mptelee  25826  neibastop1  26379  cover2  26406  upixp  26422  indexdom  26427  filbcmb  26433  mettrifi  26454  mptfcl  26768  mzpexpmpt  26793  aomclem2  27121  hbtlem5  27300  refsumcn  27668  rfcnnnub  27674  stoweidlem25  27741  stoweidlem28  27744  stoweidlem29  27745  stoweidlem31  27747  stoweidlem52  27768  stoweidlem59  27775  stoweidlem60  27776  stoweidlem62  27778  wallispilem3  27783  stirlinglem13  27802  2reu1  27931  ffnafv  28002  trintALTVD  28929  trintALT  28930  bnj228  29039  bnj1366  29138  bnj590  29218  bnj594  29220  bnj600  29227  bnj1128  29296  bnj1125  29298  bnj1145  29299  bnj1398  29340  bnj1417  29347  glbconxN  30112  pmapglbx  30503  pmapglb2xN  30506  cdlemefr29exN  31136  cdlemk36  31647
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-ral 2702
  Copyright terms: Public domain W3C validator