Theorem rsp 2773

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 2761	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		sp 1957	. 2 |- ( A. x ( x e. A -> ph ) -> ( x e. A -> ph ) )
3	1, 2	sylbi 200	1 |- ( A. x e. A ph -> ( x e. A -> ph ) )

Syntax hints:   -> wi 4   A.wal 1450   e. wcel 1904   A.wral 2756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-12 1950

This theorem depends on definitions:  df-bi 190  df-ex 1672  df-ral 2761

This theorem is referenced by:  rspa  2774  rspec  2775  r19.21bi  2776  rsp2  2780  r19.12  2903  reupick2  3720  rspn0  3735  dfiun2g  4301  iinss2  4321  invdisj  4384  trss  4499  reusv1  4601  reusv2lem1  4602  reusv2lem3  4604  reusv3  4609  ralxfrALT  4619  fvmptss  5973  ffnfv  6064  riota5f  6294  mpt2eq123  6369  peano5  6735  fun11iun  6772  wfrlem4  7057  wfrlem12  7065  tfr3  7135  tz7.48-1  7178  tz7.49  7180  nneneq  7773  scottex  8374  dfac2  8579  infpssrlem4  8754  fin23lem30  8790  fin23lem31  8791  hsmexlem2  8875  domtriomlem  8890  axdc3lem2  8899  axdc3lem4  8901  konigthlem  9011  winalim2  9139  nqereu  9372  dedekind  9815  dedekindle  9816  prodeq2ii  14044  vdwlem9  15018  mreiincl  15580  srgi  17823  ringi  17871  lbsextlem3  18461  lbsextlem4  18462  tgcl  20062  txindis  20726  alexsubALTlem3  21142  prdsxmslem2  21622  fsumcn  21980  lebnumlem1  22067  lebnumlem1OLD  22070  iscmet3lem1  22339  iscmet3lem2  22340  ovoliunlem2  22534  mbfimaopnlem  22690  limciun  22928  ftalem3  24078  ostth3  24555  mptelee  25004  ubthlem2  26594  aciunf1lem  28339  esumcvg  28981  bnj228  29615  bnj590  29793  bnj594  29795  bnj600  29802  bnj1128  29871  bnj1125  29873  bnj1145  29874  bnj1398  29915  bnj1417  29922  dfon2lem3  30502  dfon2lem7  30506  trpredmintr  30543  frr3g  30584  frrlem4  30588  frrlem11  30597  neibastop1  31086  cover2  32104  upixp  32120  indexdom  32125  filbcmb  32131  mettrifi  32150  mpt2bi123f  32470  riotasvd  32592  glbconxN  33014  cdlemefr29exN  34040  cdlemk36  34551  mptfcl  35633  aomclem2  35984  hbtlem5  36058  trintALTVD  37340  trintALT  37341  refsumcn  37414  rfcnnnub  37420  choicefi  37552  mullimc  37793  mullimcf  37800  addlimc  37826  itgsubsticclem  37949  stoweidlem25  37997  stoweidlem52  38025  stoweidlem59  38032  stoweidlem62  38035  stoweidlem62OLD  38036  wallispilem3  38041  stirlinglem13  38060  fourierdlem73  38155  2reu1  38752  ffnafv  38818