Theorem rsp 2887

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

Step	Hyp	Ref	Expression
1		df-ral 2800	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		sp 1796	. 2 |- ( A. x ( x e. A -> ph ) -> ( x e. A -> ph ) )
3	1, 2	sylbi 195	1 |- ( A. x e. A ph -> ( x e. A -> ph ) )

Syntax hints:   -> wi 4   A.wal 1368   e. wcel 1758   A.wral 2795

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794

This theorem depends on definitions:  df-bi 185  df-ex 1588  df-ral 2800

This theorem is referenced by:  rsp2  2889  rspec  2891  r19.12  2929  ralbi  2952  reupick2  3737  rspn0  3750  dfiun2g  4303  iinss2  4323  invdisj  4382  mpteq12f  4469  trss  4495  reusv1  4593  reusv2lem1  4594  reusv2lem2  4595  reusv2lem3  4596  reusv3  4601  ralxfrALT  4612  fvmptss  5884  ffnfv  5971  riota5f  6179  mpt2eq123  6247  peano5  6602  fun11iun  6640  tfr3  6961  tz7.48-1  7001  tz7.49  7003  nneneq  7597  scottex  8196  dfac2  8404  infpssrlem4  8579  fin23lem30  8615  fin23lem31  8616  hsmexlem2  8700  domtriomlem  8715  axdc3lem2  8724  axdc3lem4  8726  axdc4lem  8728  konigthlem  8836  winalim2  8967  nqereu  9202  dedekind  9637  dedekindle  9638  vdwlem9  14161  mreiincl  14645  srgi  16727  rngi  16772  lbsextlem3  17356  lbsextlem4  17357  tgcl  18699  txindis  19332  alexsubALTlem3  19746  isucn2  19979  prdsxmslem2  20229  fsumcn  20571  lebnumlem1  20658  iscmet3lem1  20927  iscmet3lem2  20928  bcthlem5  20964  ovoliunlem2  21111  mbfimaopnlem  21259  limciun  21495  ftalem3  22538  ostth3  23013  mptelee  23286  ubthlem2  24417  esumcvg  26673  prodeq2ii  27563  dfon2lem3  27735  dfon2lem7  27739  trpredmintr  27832  wfrlem4  27864  wfrlem12  27872  frr3g  27904  frrlem4  27908  frrlem11  27917  heicant  28567  neibastop1  28721  cover2  28748  upixp  28764  indexdom  28769  filbcmb  28775  mettrifi  28794  mpt2bi123f  29116  mptfcl  29197  mzpexpmpt  29222  aomclem2  29549  hbtlem5  29625  refsumcn  29893  rfcnnnub  29899  stoweidlem25  29961  stoweidlem28  29964  stoweidlem29  29965  stoweidlem31  29967  stoweidlem52  29988  stoweidlem59  29995  stoweidlem60  29996  stoweidlem62  29998  wallispilem3  30003  stirlinglem13  30022  2reu1  30151  ffnafv  30218  trintALTVD  31919  trintALT  31920  bnj228  32029  bnj1366  32126  bnj590  32206  bnj594  32208  bnj600  32215  bnj1128  32284  bnj1125  32286  bnj1145  32287  bnj1398  32328  bnj1417  32335  riotasvd  32916  glbconxN  33331  pmapglbx  33722  pmapglb2xN  33725  cdlemefr29exN  34355  cdlemk36  34866